Introduced "class_table" and "feature_table"

	new file:   ocaml/class_table.ml
	new file:   ocaml/class_table.mli
	modified:   ocaml/container.ml
	modified:   ocaml/eiffelc.ml
	new file:   ocaml/feature_table.ml
	new file:   ocaml/feature_table.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml
	modified:   ocaml/term.ml
	modified:   ocaml/type.ml
Improved class_table and feature_table and added assertion_table so that the first proofs can be started

	modified:   library/kernel/boolean.e
	new file:   ocaml/assertion_table.ml
	new file:   ocaml/assertion_table.mli
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/container.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof.ml
	modified:   ocaml/support.ml
	modified:   ocaml/term.ml
	modified:   ocaml/type.ml
	modified:   ocaml/verify.ml
Added some thoughts on how to find proofs

	modified:   library/kernel/boolean.e
	modified:   ocaml/proof.ml
First proof of 'a=>' successful, but structures need to be improved

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/container.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof.ml
	modified:   ocaml/term.ml
Automatic proofs for implication with forward reasoning implemented

The prover can now prove all boolean assertions of the kind

    a=>a
    (a=>b) => (b=>c) => (a=>c)
    (a=>b) => (a=>b=>c) => c

by applying forward reasoning. Endless loops in the closure of the term map are detected.

Backward reasoning is implemented, but endless loop detection still needs to be implemented.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Automatic proofs for implications with forward reasoning implemented

The prover can now prove all boolean assertions of the kind

    a=>a
    (a=>b) => (b=>c) => (a=>c)
    (a=>b) => (a=>b=>c) => c

by applying forward reasoning. Endless loops in the closure of the term map are detected.

Backward reasoning is implemented, but endless loop detection still needs to be implemented.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Merge branch 'develop' of github.com:hbr/modern-eiffel into develop

Corrected a typo and commited with amend after pushing to the remote repo.
Backward reasoning now complete with endless loop detection

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/feature_table.ml
Expansion of function definitions implemented

Functions in terms can be replaced by their definitions (i.e. lambda terms
are inserted as the functions). The term_to_string function has been
completed to allow the printing of lambda terms. However the types of
the lambda terms are still missing.

Reduction of lambda terms is not yet implemented.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/container.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/term.ml
Bugfix: Anonymous variables must be the complement of de Bruijn indices

Internally de Bruijn indices are used as variable names. In an environment with
n anonymous variables we use the names @0, @1, ... @n-1 as external representation
but the corresponding de Bruijn indices are n-1, n-2, ... 0.

	modified:   ocaml/feature_table.ml
Added proof tracing, function expansion and beta reduction

1. Proofs can be traced. There is a trace flag. If it is not set the prover
   starts without tracing. If it cannot proof an assertion it sets the
   trace flag and restarts the proof.

2. Functions can be expanded i.e. all function symbols which have a definition
   are replaced by the corresponding lambda term.

3. Beta reduction means applying all lambda terms to their arguments.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/term.ml
Proof engine works internally with normalized terms, clean up

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
Improved tracing of proofs and replaced 'assert false' by a more readable error message

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/feature_table.ml
Fix: Loop detection in backward reasoning was too restrictive

Reason for loop detection:

If the prover tries to prove the assertion

   all(a,b:BOOLEAN) (a=>b) => (b=>a) => a

it shifts 'a=>b' and 'b=>a' into the context and tries to prove a.
Backward reasoning says that I can prove 'a' by proving 'b' and I
can prove 'b' by proving 'a'. Without a loop detection this procedure
can loop forever.

The first loop detection stored the set of a term which are still to
be proved to prove the current goal. In the second iteration the prover
tries to prove 'a' and with the set of still to be proved goals {a,b}.
Since 'a' is already in the set the prover fails because it has a loop
detected.

In the above example the loop detection is correct. However we get a
different story if we try to prove

    all(a) not not not a => not a

without classical logic. The normalized form of the assertion is

    all(a) (((a=>false)=>false)=>false) => a => false.

By shifting two assumptions into the context we get

    ((a=>false)=>false)=>false, a |- false

Backward reasoning allows the step

    ((a=>false)=>false)=>false, a |- (a=>false)=>false

Shifting the antecedent and closing the context yields

    ((a=>false)=>false)=>false, a, a=>false, false |- false

In this context we have 'false' in the set of still to be proved assertions
and the restrictive loop detector bails out. But this is too
restrictive because we have a richer context now (there are two
assumptions more in the context than in the previous state where
the prover tried to prove 'false'). Even the goal is already among
the assumptions. I.e. the prove can succeed.

Solution: Instead of a set of still to be proved goals we use a map
which maps the still to be proved goals to the context where they
have been tried to prove. If the context is now richer the prover
does continue.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
Fix: The keyword 'not' can start a new statement

The lexer on looking at

    a => a
    not a

must inject an invisible semicolon before returning 'not' to the parser. I.e.
the lexer must recognize the keyword 'not' as a token which can start
a new statement but cannot end a statement.

	modified:   library/kernel/boolean.e
	modified:   ocaml/lexer.mll
Some clean up and explicit "not yet implemented" error messages

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
Minor bugfix in calculating de Bruijn indices

	modified:   ocaml/feature_table.ml
	modified:   ocaml/term.ml
Minor edit
Splitted assertion_table into assertion_table and prover

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/eiffelc.ml
	renamed:    ocaml/assertion_table.ml -> ocaml/prover.ml
	new file:   ocaml/prover.mli
Prover finds exact matches of the current goal in the global assertion table

This is done via unification and by looping through all assertions in the
assertion table. The algorithm needs improvement in the future because
it is not very efficient.

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/class_table.ml
	modified:   ocaml/proof.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml