Added focussed beta reduction

The prover will do a toplevel beta reduction in forward and in backward
direction if possible.

The feature is not yet active because the prover beta reduces all terms
before applying forward and backward reasoning.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/term.ml