Fix: Duplicate inheritance clause caused problems

A duplicate inheritance clause must not have any effect because the inheritance
has already been done.

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Entering of deferred functions checked more thoroughly

- Only entered in the same module as the owner class
- Not entered if the owner class has already descendants

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table.mli
Inhibit inheritance to public classes in implementation files

Inheritance to public classes (i.e. classes which have been defined in
some of the used modules) is not allowed in implementation files, because
the inheritance puts classes as ancestors to publicly visible classes which
users of the implemented module might not be able to see.

Note: This strict rule might be made more specific in the future.

Furthermore: Removal of unneeded functions.

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
Push variants of functions to all descendants

Functions of a certain owner class can be added in other modules than
the module of the owner class. The added features have to be effective.

In case that the owner class already has descendants a variant of the
added function is inserted into the descendant classes as well.

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Formal generics moved from class table to module table

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/module_table.ml
	modified:   ocaml/module_table.mli
Some minor refactorings and cleanups

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/support.ml
	modified:   ocaml/typer.ml
Moved module 'Context' into module 'Proof_table'

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/eiffelc.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
Refactored 'check_deferred'

All checks for deferred features/assertions are now done in one function.

A feature can be deferred only if

- the owner class is deferred
- it is defined in the same module as the owner class
- the owner class does not yet have descendants
- there is a unique formal generic anchored in the owner class

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/prover.ml
Improved error messages with header marks

The header mark get the same file info as the class name. With this
the file info is useful even if no header mark is present.

	modified:   ocaml/parser.mly
Added assertion inheritance

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/eiffelc.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
Fix: unifier in term table

The term table has a set of schematic terms i.e. terms with variables which
can be substituted.

Unification is done by checking a term to be unified from top to bottom
according to its structure. Whenever there is a variable of a schematic term
in the table at the corresponding position a substitution is generated for the
variable. However this is incorrect if the substitution contains bound
variables of the term to be checked. No term with bound variables can
substitute a variable!

	modified:   ocaml/term_table.ml
Push and pop to module 'Context' done via 'Proof_table'

The module 'Proof_context' does no pushs and pops directly to the
module 'Context'.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Assumptions are push all and then all closed

Old algorithm: Each assumption pushed to the context had been forward
closed immediately. This had the consequence that the assumptions did
not appear as one block in the context.

New: algorithm: All assumptions are pushed en bloque and then closed en
bloque. Therefore all assumptions of a subproof appear en bloque in the
context.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/prover.ml
Proof term with base index and term reconstruction

Each proof term has a base index. The base index points to the position
in the proof table for which the proof term has been constructed.

Since proofs can have multiple ensure clauses a proof can result in various
proof terms, one for each ensure assertion. All these proof terms have the
same base index. But only one of them can be put at the base index and the
others at 'base_index + 1' ...

All references below the base index are absolute. All references above the
base index have to be shifted up by 'i' if the proof term has to be inserted
at 'base_index + i'.

Term reconstruction from a proof term has been reimplemented in a way that it
allows printing of proof terms as proofs of the source language.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover.ml
Functions for focussed expansion prepared

(not yet activated)

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof_table.ml
Removed unnecessary context pushs from alternative processing

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover.ml
Fix: entering and discharged proof term

If the prover enters a term (i.e. breaks up an implication chain) it
has to push the assumptions into a clean context.

The discharged proof term did not contain enough terms in case that
the goal was among the assumptions and there were more assumptions to
come.

	modified:   ocaml/proof_table.ml
	modified:   ocaml/prover.ml
Allowing backward rules which do not simplify and not introduce

Now all backward rules are allowed as long as the target is the shortest
tail which contains all argument variables and is simplifying or not a single
variable (no catchall rules i.e. still no automatic indirect proofs possible).

The backward rules are still classified as simplifying (i.e. the node count
of any premise is not greater than the node count of the target) and non
simplifying.

The non simplifying rules cannot be used repeately to avoid infinite loops
in the verifier.

	modified:   ocaml/proof_context.ml
Fix: Parenthesis around operator expressions when in function position

E.g. in predicate: (-p)(x) is correct, - p(x) is false, because
the parenthesis operator '()' binds stronger than any operator.

	modified:   ocaml/feature_table.ml