Fix: Wrong sequence in handling exceptions in the term unifier

	modified:   ocaml/term.ml
Activated function expansions within the operands of boolean 'or'

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof_context.ml
Made all relational operators non associative

	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml
Cleanup of the lexer and parser

The implication symbol is '==>' (and not '=>')

The keyword to introduce a proof is 'proof' (and not 'check')

	modified:   ocaml/lexer.mll
	modified:   ocaml/parser.mly
Functions with precondition and no definition allowed

	modified:   ocaml/ast.ml
Added comment

	modified:   ocaml/support.ml
Fix: Parsing of predicate expressions with multiple arguments

	modified:   ocaml/parser.mly
Improved trace output

	modified:   ocaml/alba.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/proof_context.ml
Abreviation 'PC = Proof_context' eliminated

	modified:   ocaml/ast.ml
Refactored feature inheritance

Feature inheritance cannot be done completely in the module 'Feature_table'
because in case of a feature redefinition it has to be proved that
the original definition in the ancestor and the definition in the heir
are equivalent. Therefore access to the prover is needed and the module
'Feature_table' cannot have access to the prover.

Therefore the basic control functions for feature inheritance have been
put into a new module 'Inherit' which has access to the prover.

	modified:   ocaml/ast.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	new file:   ocaml/inherit.ml
	new file:   ocaml/inherit.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml
Fix: Correct parentheses inserted in the term printer

... for nonassociative operators

	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/term_table.ml
Allowed insertion in arbitrary sequence into 'Term_table'

The indices do not any more have to be inserted in ascending order
into term tables. However it is still not allowed to insert duplicate
indices.

	modified:   ocaml/term_table.ml
Added 'flush_all' after toplevel trace messages

This has the effect that at least the message 'Compile module ...'
are visible immediately without output buffering.

	modified:   ocaml/alba.ml
Equivalence of redefined functions verified

A heir can inherit a feature and overide the definition of the
ancestor. In this case it has to be proved that the redefined and
the original feature are equivalent.

	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
	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Some cleanup

	modified:   ocaml/term_builder.ml
Fix: Missing exception handling in 'alba.ml'

	modified:   ocaml/alba.ml
	modified:   ocaml/module_table.ml
Fix: Check term equivalence with alpha equality only

Two terms are equivalent even if they have different names for their
bound variables.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/term.ml
Added copyright note to all source files

	modified:   ocaml/alba.ml
	modified:   ocaml/ast.ml
	modified:   ocaml/container.ml
	modified:   ocaml/context.ml
	modified:   ocaml/inherit.ml
	modified:   ocaml/inherit.mli
	modified:   ocaml/lexer.mll
	modified:   ocaml/map_table.ml
	modified:   ocaml/map_table.mli
	modified:   ocaml/module_table.ml
	modified:   ocaml/module_table.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/rule_data.ml
	modified:   ocaml/rule_data.mli
	modified:   ocaml/support.ml
	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table.mli
	modified:   ocaml/term_table2.ml
	modified:   ocaml/term_table2.mli
	modified:   ocaml/tvars.ml
	modified:   ocaml/tvars.mli
	modified:   ocaml/typer.ml
Minor edit

	modified:   ocaml/lexer.mll
Fix: Toplogical sort of modules

	modified:   ocaml/alba.ml