Fix: Partial specialization not done correctly in some boundary cases

If we have the proved assertion

    all(a) false => a

and have `false` in the context the forward prover should trigger
a partial specialization of the above assertion which looks like

    false => all(a) a

i.e. it is an implication and can used as the implication term of the
modus pones rule resulting in `all(a) a` with `false` in the context.

Since the partial specialization has not been done correctly, the prover
inserted

    all(a) false => a

into the context which is not an implication and results in an error
in applying the modus ponens rule.

	modified:   ocaml/proof_context.ml
Added parsing of interface files

	modified:   ocaml/eiffelc.ml
	modified:   ocaml/lexer.mll
	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/prover.ml
Some cleanups in 'container.ml'

Added complete function signatures (i.e. argument and return types)

Changed the order of arguments in order to be more inline with the
standard lib of ocaml. E.g. 'Seq.elem i seq' instead of
'Seq.elem seq i'.

	modified:   ocaml/class_table.ml
	modified:   ocaml/container.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/parser.mly
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/support.ml
Minor adaption to the grammar

Currently the grammar does not accept

    all(a) check  ... ensure ... end
    all(a) ensure ... end

as subproofs within a proof. The adaption enables at least the first
one. The second one requires a major rework of the grammar.

	modified:   ocaml/parser.mly
Removed assertion to detect long running forward reasoning

	modified:   ocaml/context.ml
Fix: unifier with bound variables

If the term to be unified with the terms in the table has a bound
variable at a certain position and there are no terms in the table
have the same bound variable at this position, then the term is not
unifyable.

	modified:   ocaml/term_table.ml
Fix: basic prover

'add_consequences_premise' has to be called always. The restriction
implemented before is not valid.

	modified:   ocaml/context.ml
	modified:   ocaml/proof_context.ml
Removed some unnecessary functions

	modified:   term.ml
Some minor performance improvements in the unifier

The exception 'Not_found' is raised as soon as there are no matching
terms (for the function term or one of the argument terms) possible.

	modified:   ocaml/term_table.ml
Renaming of some record selectors

	modified:   ocaml/proof_context.ml
Added slots to 'proof_context.ml'

Added some alternative code to make some of the tables based on
TermMap's. The alternative code has been tried on 'find', but no
difference of performance resulted.

The alternative code has been left in, because it might be more
effective on some of the other tables used for backward and forward
reasoning.

	modified:   ocaml/proof_context.ml
Added 'join_lists' and 'merge_lists'

... as an alternative to 'join_map' and 'merge_map'.

The code is not yet activated.

	modified:   ocaml/term_table.ml
Replaced maps by lists in 'term_table.ml'

Instead of using maps from indices to substitutions we use lists of
pairs 'idx,sub'. This nearly doubles the performance of the unifier.

	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table.mli
Removed some unnecessary files

	deleted:    ../library/kernel/kernel.eml
	deleted:    arguments.ml
	deleted:    arguments.mli
	deleted:    main.ml
	deleted:    validate.ml
	deleted:    verify.ml
Cleanup of the grammar

Removed a lot of no longer needed constructs:

- visibility
- nested declaration blocks
- tagged expressions

Cleanup of the expression and assertion rules.

	modified:   context.ml
	modified:   context.mli
	modified:   eiffelc.ml
	modified:   feature_table.ml
	modified:   feature_table.mli
	modified:   parser.mly
	modified:   prover.ml
	modified:   support.ml
Used a for loop instead of a recursive function

... and used 'list=[]' instead of 'Mylist.is_empty list'.

	modified:   typer.ml
	modified:   signature.ml
	modified:   context.ml
	modified:   class_table.ml
	modified:   signature.ml
Editorial

Deleted comments, replaced recursive function by a loop.

	modified:   ocaml/context.ml
	modified:   ocaml/typer.ml
Removed 'proof.ml' which is no longer necessary

	modified:   ocaml/context.ml
	deleted:    ocaml/proof.ml
Prepared coded for inheritance and modules

- Moved unification of type expressions to 'typer.ml'
- Fixed a bug in the unifier with formal generics

	modified:   library/kernel/any.e
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/signature.ml
	modified:   ocaml/term.ml
	modified:   ocaml/typer.ml
Deleted some unnecessary comments

	modified:   ocaml/term.ml