Term simplification introduced into the prover

A simplification rule is a equality where the right hand side is
strictly simpler than the left hand side. Such a rule can be used
to simplify expressions.

The simplification is part of the evaluation of an expression and
therefore applied of forward and in backward direction.

	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Added unification algorithm to 'term.ml'

	modified:   ocaml/term.ml
Used 'Context' to expand function definitions and terms

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/rule_data.ml
	modified:   ocaml/rule_data.mli
Disallowed silly backward rules

Rules of the form

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

are not used as backward rules because a premise has the same structure
as the target i.e. can be unified with the target and the substitution
is nontrivial. For first premise of the above case we get the substitution

    a ~> a*b,   b ~> a

i.e. at the position of the variable 'a' in the target appears a term
which is just blown up. Since the premises have the same structure as
the target the prover shall not try this rule for backward reasoning.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/rule_data.ml
	modified:   ocaml/term.ml
Deletion
	deleted:    ocaml/eiffelc.ml
Added 'false', 'not' and 'or' to the basic functions

	modified:   ocaml/feature_table.ml