renamed print_lthms to print_facts, do not insist on proof state;

renamed Toplevel.enter_forward_proof to Toplevel.enter_proof_body;

renamed Toplevel.enter_forward_proof to Toplevel.enter_proof_body;

print_evaluated_term: Toplevel.context_of;

replaced attributes_update by map_attributes;

Toplevel.local_theory_to_proof: proper target;

Toplevel.local_theory: proper target;

removed dead code;

removed dead code;

To be consistent with "induct", I renamed "fixing" to "arbitrary".

However I am not very fond of "arbitrary" - e.g. it clashes with

"arbitrary" of HOL. Both Gentzen (at least in the Szabo translation)

and Velleman (in How to prove it: a structured approach) use

"arbitrary".

Still, I wonder whether "generalising" is a good compromise?

However I am not very fond of "arbitrary" - e.g. it clashes with

"arbitrary" of HOL. Both Gentzen (at least in the Szabo translation)

and Velleman (in How to prove it: a structured approach) use

"arbitrary".

Still, I wonder whether "generalising" is a good compromise?

Extended combinators now disabled

abstraction is now turned OFF...

Logging of theorem names to the /tmp directory now works

cc: avoid space after options;