Improved help text

	modified:   ocaml/alba.ml
Improved checking of actual generics

	modified:   ocaml/class_table.ml
Removed unused parts of 'Support.type_t'

	modified:   ocaml/module_table.ml
	modified:   ocaml/support.ml
Minor edit

	modified:   ocaml/proof_context.ml
Implemented 'some elimination' into the proof engine

Whenever the proof engine has a statement of the form

    some(a,b,...) e1

in the context it puts the statement

    all(e2) (all(a,b,...) e1 => e2) => e2

into the context.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Fix: Allowed complete forward reasoning with a backward rule

A backward rule might be not simplifying in forward direction. But
it must be always possible to complete the forward reasoning with
a backward rule. For this purpose it has been inserted. The prover
iterates through all premises of a backward rule. Each proved premise
triggers one forward reasoning until the goal is in the context.

Consider the backward rule 'a => b => c' which has been inserted for
the goal 'c'. The prover tries to prove 'a' and in case of success puts
it into the context. The forward close puts then 'b => c' into the context.
Then then prover tries to prove 'b' puts it into the context. The forward
close then puts 'c' into the context and we are ready. If the forward
reasoner blocks for any reason the insertion of 'b => c' then the process
cannot be terminated successfully. Therefore there must not be any blocking
for the intermediate steps of processing a backward rule for a certain
target.

	modified:   ocaml/proof_context.ml