Implemented some commandline options and and improved loop detector

1. Tracing can be set via a command line option (-trace proof  -trace failed-proof)

2. There are still some issues with combinatorial explosion

It has to be analyzed more thoroughly how big the search path of the prover
has to be. With our current definition of boolean functions (only implication
as a basic function and all others based on this) it is easy to push the
prover to its limit. The prover now expands all boolean expressions to
contain only implications. This makes the terms very big and allows the
prover a lot of alternatives to explore.

Some options:

a) Make all the boolean functions basic with the corresponding introduction
   and elimination rules

b) Try a two (multi) stage definition of the boolean functions so that the
   higher stage has no access to the definitions of the lower stage. The
   same effect could be achieved by making function definitions which
   are visible only in the feature block (problem with syntactic ambiguity).

	modified:   library/kernel/boolean.e
	modified:   ocaml/assertion_table.ml
	modified:   ocaml/container.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/prover.ml
There is an error in Term.normalize: Instrumented and commented out

	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
Added boolean module with introduction and elimination rules

The module 'boolean1.e' defines all boolean functions as basic
functions and defines their behaviour via axioms. This approach
seems to be far better suited than the approach which defined
only '=>' as a basic function.

	modified:   ocaml/assertion_table.ml
	new file:   ocaml/boolean1.e
Statistics and goal limits implemented

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/support.ml