Renamed Assertion_context -> General_context, Proof_context -> Local_context

	modified:   ocaml/assertion_table.ml
	renamed:    ocaml/assertion_context.ml -> ocaml/general_context.ml
	renamed:    ocaml/assertion_context.mli -> ocaml/general_context.mli
	renamed:    ocaml/proof_context.ml -> ocaml/local_context.ml
	renamed:    ocaml/proof_context.mli -> ocaml/local_context.mli
	modified:   ocaml/prover.ml
Added only the match part of an implication to the backward rules

Assume we have a general rule of the form 'a=>b=>...=>z'. The match
part is the shortest tail which contains all argument variables of the
rule. Only the match part is entered into the set of backward rules of
a general context because the application of a backward rule should not
leave any argument variables open.

A bug in the function 'Term.implication_chain' has been discovered and
fixed

	modified:   ocaml/general_context.ml
	modified:   ocaml/term.ml
Introduced substitutions instead of argument arrays in proof terms

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/general_context.ml
	modified:   ocaml/general_context.mli
	modified:   ocaml/proof.ml
Added some functions to apply substitutions

	modified:   ocaml/proof.ml
	modified:   ocaml/term.ml
Added draft code for the new prover

	new file:   ocaml/new_prover.ml