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