First version of 'Proof_context' added

The proof context is already part of the context, but participates
up to now only in the push and pop operations.

	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	new file:   ocaml/proof_context.ml
	new file:   ocaml/proof_context.mli
Removed unnecessary type 'key'

	modified:   ocaml/feature_table.ml
Then array representing the argument names is always consistent

By entering a proof context it is never possible that the array
representing the argument names is empty and then variable 'nbenv'
is different from zero.

	modified:   ocaml/proof_table.ml
Added function and variable renaming

- Added the function 'push_empty' to push a context without any
  new variables.

- The variable 'c' is used consistently to describe the context and
  not 'loc' as previously.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
Corrected printing of quantified terms

	modified:   ocaml/feature_table.ml
	modified:   ocaml/support.ml
Various changes in the context tables to be a good infrastructure for the prover

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/term.ml
	modified:   ocaml/typer.ml
Added function 'add_proved' and a fix

fix: The field 'entry' in the module 'Proof_context' has mutable
     subfields. I.e. if the 'entry' is stacked it has to be stacked
     as a copy. Otherwise the subfields of the stacked entry and the
     current entry will be modified.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/term_table0.ml
Fix: 'Term.binary' put the left and right operand in the wrong order

	modified:   ocaml/term.ml
Fix: Some typos which led to wrong behaviour

	modified:   ocaml/proof_context.ml
	modified:   ocaml/term_table0.ml
Added draft version of the new prover

The new prover which is base on the modules 'Context', 'Proof_context'
and 'Proof_table' is not yet activated but added for test purposes.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	new file:   ocaml/prover2.ml
Fixed precedence of 'all' and 'some'

'all' and 'some' must have a higher precedence than '=>'.

	modified:   ocaml/support.ml
Fix: Bug in printing of anonymous variables

	modified:   ocaml/feature_table.ml
Improved readability of 'specialized_forward'

	modified:   ocaml/proof_context.ml
Fix: Update of type variable only if set

	modified:   ocaml/signature.ml
	modified:   ocaml/term.ml
Fix: Substitutions now applied in 'update_type_variables'

The type inference infers the type of untyped variables. But the
inferred types also have to be applied to the 'argtypes' in order
to be visible effective.

	modified:   ocaml/context.ml
	modified:   ocaml/signature.ml
	modified:   ocaml/term.ml
New prover tested with prover 'basic' on some examples

- Subproofs not yet implemented

- Iterated backward reasoning not yet implemented

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover2.ml
	modified:   ocaml/support.ml
	modified:   ocaml/term_table0.ml
Added the possibility to verify subproofs to the new prover

An assertion feature can now have the form

     all(a,b,...)
         require
	     ...
         check
             ...
             all(x,y) require ... check ... ensure ... end
             require ... check ... ensure ... end
             ...
         ensure
             ...
         end

	modified:   ocaml/context.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/prover2.ml
Made sure that only equivalent assertions are inserted into the context

The terms

    all(a,b) a and b => b and a

    all(a,b) b and a => a and b

are equivalent. Only one of them should be in the context.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
New prover in basic mode tested on some examples

	modified:   ocaml/context.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/prover2.ml
Added function 'is_assumption'

	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli