Clean up

	modified:   ocaml/class_table.ml
Added information to the trace of the typer

	modified:   ocaml/typer.ml
Fix: No circular substitutions allowed

The term builder ignored the case that a type variable is substituted
by itself. This created circularity in the substitution.

Furthermore the substitution did not check for circularity (which it
should do).

	modified:   ocaml/signature.ml
	modified:   ocaml/term_builder.ml
Upgrading of function signatures to a predicate or a function

	modified:   ocaml/feature_table.ml
	modified:   ocaml/proof_context.ml
Fix: Preconditions of functions typed correctly

The result type of an assertion is always BOOLEAN, and usually not
the result type of the function.

	modified:   ocaml/ast.ml
	modified:   ocaml/term_builder.ml
	modified:   ocaml/term_builder.mli
	modified:   ocaml/typer.ml
Added code to detect transitivity rules

Basic idea: use transitivity rules only in forward direction even
if they are not strictly simplifying.

Unfortunately the runtime does not improve if we activate this feature.
Therefore the code is just in and not activated to guide the prover.

The inefficiency in some cases has to be analyzed more in depth to
find a good solution.

	modified:   ocaml/rule_data.ml
	modified:   ocaml/rule_data.mli
	modified:   ocaml/term.ml
Fix: Normalization of proof terms

The normalization did not work correctly when the proof term was
and axiom with a universally quantified term.

	modified:   ocaml/proof_table.ml
Verification of ghost inheritance implemented

	modified:   ocaml/ast.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.mli
	modified:   ocaml/inherit.ml
	modified:   ocaml/inherit.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
Added code to detect base features for compliance check with '='

Base features of a class are features which do not have a definition.

If the class inherits from ANY then all these features have to be
consistent with equality so that the leibniz rule is valid.

The detection of base features has been implemented but the
consistency check with '=' is not yet implemented.

	modified:   ocaml/ast.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/inherit.ml
	modified:   ocaml/inherit.mli
Introduced the module 'Feature'

	modified:   ocaml/ast.ml
	new file:   ocaml/feature.ml
	new file:   ocaml/feature.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/support.ml
Included builtin definition of 'and' and added precondition support

	modified:   context.ml
	modified:   context.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli