Eliminated "catch all" rules from forward and backward rules

The rules

    all(a:BOOLEAN) a => not a => false
    all(a:BOOLEAN) (not a => false) => a

are "catch all" rules. The first one is a catch all forward rule because it allows from
any term 'a' in the context to conclude 'not a => false'. These forward rules just double
the size of the contexts and do not add value (or very limited value). The second one
is a "catch all" backward rule. Every goal 'a' can be proved by proving 'not a => false'.
If this rule were allowed then the prover would try to prove any goal indirectly by assuming
the opposite a deriving false. These rules are not treated as valid backward rules. Therefore
the user has to say explicitly if he wants an indirect proof of an assertion.

	modified:   ocaml/general_context.ml
Made General_context generic to store some user specific information with the assertions

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/general_context.ml
	modified:   ocaml/general_context.mli
	modified:   ocaml/proof.ml
	modified:   ocaml/term.ml