removed obsolete Toplevel.enter_proof_body;

standardized pretty printing of consts (e.g. see find_theorems, print_theory);

misc tuning and simplification;

simplified/unified command setup;

removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);

prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining; tuned;

prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;

tuned eval_thms (cf. note etc. in proof.ML);

use Pretty.enum convenience;

tuned whitespace;