haftmann [Wed, 11 Aug 2010 08:58:18 +0200] rev 38338
remove overloading and instantiation from data slot
wenzelm [Wed, 11 Aug 2010 18:11:07 +0200] rev 38337
removed obsolete Toplevel.enter_proof_body;
wenzelm [Wed, 11 Aug 2010 18:10:39 +0200] rev 38336
standardized pretty printing of consts (e.g. see find_theorems, print_theory);
wenzelm [Wed, 11 Aug 2010 18:03:02 +0200] rev 38335
misc tuning and simplification;
wenzelm [Wed, 11 Aug 2010 17:50:29 +0200] rev 38334
simplified/unified command setup;
wenzelm [Wed, 11 Aug 2010 17:37:04 +0200] rev 38333
removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
wenzelm [Wed, 11 Aug 2010 17:31:56 +0200] rev 38332
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;
wenzelm [Wed, 11 Aug 2010 17:29:54 +0200] rev 38331
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm [Wed, 11 Aug 2010 17:24:57 +0200] rev 38330
tuned eval_thms (cf. note etc. in proof.ML);
wenzelm [Wed, 11 Aug 2010 15:17:13 +0200] rev 38329
use Pretty.enum convenience;