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