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