Experimental code for assertion table added as new module 'term_table'

The code is used in the context of the prover to store the proved
assertions. It is not yet used in the assertion table. The unification
part of the term_table is not yet used.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
	new file:   ocaml/term_table.ml
	new file:   ocaml/term_table.mli
Reindexing of arguments

Function application is described by the term 'Application(f,args)' where args
is an array and the argument i is args.(i). Since we are using de Bruijn
indices this does not map well because the de Bruijn index of argument i is
n-1-i.

Therefore the order of the argument array has been reversed so that args.(i)
refers to the de Bruijn index i i.e. to the argument n-1-i.

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/term.ml
Removal of type array in lambda expressions

The type array in lambda expression like 'Lam(tarr,t)' has been replaced by
the number of arguments 'Lam(nargs,t)'. The types are not necessary because
only well typed terms can pass the type checker/inferer and all term
transformations generate only well typed terms.

	modified:   ocaml/feature_table.ml
	modified:   ocaml/term.ml
Fix: Binary operators not been adapted for reindexing

... and added 'term_table' to 'assertion_table' (not yet complete)

	modified:   ocaml/feature_table.ml
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/proof.ml
	modified:   ocaml/term.ml
	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table.mli
	modified:   ocaml/proof.ml
Removed attempt map completely from the prover

	modified:   ocaml/prover.ml
Statistics added to count failed goals

	modified:   ocaml/prover.ml
	modified:   ocaml/support.ml