Fri, 06 Jan 2006 18:18:14 +0100 removed obsolete eqrule_FOL_data.ML;
wenzelm [Fri, 06 Jan 2006 18:18:14 +0100] rev 18596
removed obsolete eqrule_FOL_data.ML;
Fri, 06 Jan 2006 18:18:13 +0100 simplified EqSubst setup;
wenzelm [Fri, 06 Jan 2006 18:18:13 +0100] rev 18595
simplified EqSubst setup;
Fri, 06 Jan 2006 18:18:12 +0100 obsolete, reuse mk_rews of local simpset;
wenzelm [Fri, 06 Jan 2006 18:18:12 +0100] rev 18594
obsolete, reuse mk_rews of local simpset;
Fri, 06 Jan 2006 15:18:22 +0100 Toplevel.theory_to_proof;
wenzelm [Fri, 06 Jan 2006 15:18:22 +0100] rev 18593
Toplevel.theory_to_proof;
Fri, 06 Jan 2006 15:18:21 +0100 transactions now always see quasi-functional intermediate checkpoint;
wenzelm [Fri, 06 Jan 2006 15:18:21 +0100] rev 18592
transactions now always see quasi-functional intermediate checkpoint; removed obsolete theory_theory_to_proof; added
Fri, 06 Jan 2006 15:18:20 +0100 tuned EqSubst setup;
wenzelm [Fri, 06 Jan 2006 15:18:20 +0100] rev 18591
tuned EqSubst setup;
Fri, 06 Jan 2006 15:18:19 +0100 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm [Fri, 06 Jan 2006 15:18:19 +0100] rev 18590
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
Thu, 05 Jan 2006 22:30:00 +0100 hide type datatype node;
wenzelm [Thu, 05 Jan 2006 22:30:00 +0100] rev 18589
hide type datatype node; added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy; no_body_context: no history; transaction: test save = true;
Thu, 05 Jan 2006 22:29:59 +0100 tuned print_theorems_theory;
wenzelm [Thu, 05 Jan 2006 22:29:59 +0100] rev 18588
tuned print_theorems_theory;
Thu, 05 Jan 2006 22:29:58 +0100 Toplevel.proof_position_of;
wenzelm [Thu, 05 Jan 2006 22:29:58 +0100] rev 18587
Toplevel.proof_position_of;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip