Improved documentation

	modified:   ocaml/container.ml
Added 'least_free' which returns the least free variable of a term

	modified:   ocaml/term.ml
Use backward rules only once

In a context we might have various backward rules for a target

    a => b => t
    c => t

This gives raise to alternatives in the proof search. In the example we have
two alternatives to prove 't'. Either proof 'a' and 'b' or proof 'c'.

During each alternative we might encounter the same target again. If we allow
all backward rules we can use the same rule over and over again.

Therefore if we enter an alternative we mark the corresponding backward rule
as used and don't allow its usage in further down.

	modified:   library/kernel/boolean.e
	modified:   ocaml/local_ass_context.ml
	modified:   ocaml/local_ass_context.mli
	modified:   ocaml/prover.ml
	modified:   boolean1.e
Linear search in arrays now done with predicates

Now we find an index for an element which satisfies a predicate instead
of being equal to some given value.

	modified:   ocaml/class_table.ml
	modified:   ocaml/container.ml
	modified:   ocaml/local_context.ml
Performance improvement

In the term table we store for all bounded and free variables of a node
already a map to empty substitutions for each assertion id instead of
just the set of assertion ids. Therefore during unification the map is
already available instead of being generated on the fly. This nearly
doubles the performance of the prover.

	modified:   ocaml/term_table0.ml
Added some functions

	modified:   ocaml/term.ml
Added 'proof_table.ml'

	new file:   ocaml/proof_table.ml
	new file:   ocaml/proof_table.mli
Added 'fold_with_level' to 'term.ml'

Sometimes it is necessary to know the level from the root node
while folding the free variables of a term (e.g. to see if an
operation has been distributed over some other i.e. if the
operation appears on a deeper level than before)

	modified:   ocaml/term.ml
Added 'equal_wo_names' to 'term.ml'

	modified:   ocaml/term.ml
Completed 'unify_with'

The function 'unify_with' requires for each node to know the subterms
which belong to that node. This is necessary because the node might
match with a variable of the term for which substitutions have to be
found. In this case all the subterms which can substitute the variable
have to be returned.

	modified:   ocaml/term_table0.ml
Used the library function 'cardinal' instead of a self written function

	modified:   ocaml/term.ml
Added some functions to 'Proof_table'

	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Removal of some unneeded code and some simplifications

	modified:   ocaml/context.ml
	modified:   ocaml/typer.ml
Moved some functions from 'Context' to 'Local_context'

This is one step in order to eliminate 'Context' in its current
setting.

	modified:   ocaml/context.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/local_context.ml
	modified:   ocaml/local_context.mli
	modified:   ocaml/typer.ml
Removed 'Context' from the system and used 'Local_context' instead

	modified:   ocaml/eiffelc.ml
	modified:   ocaml/local_context.ml
	modified:   ocaml/local_context.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/prover.mli
	modified:   ocaml/typer.ml
	deleted:    ocaml/context.ml
Renamed 'Local_context' to 'Context'

The module 'Local_context' stores all contexts, the global and all
local contexts. Therefore it represents the *context*.

	renamed:    ocaml/local_context.ml -> ocaml/context.ml
	renamed:    ocaml/local_context.mli -> ocaml/context.mli
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/prover.mli
	modified:   ocaml/typer.ml
Removed the 'new_prover' because it is overcome by events

	deleted:    ocaml/new_prover.ml
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