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
wenzelm [Fri, 06 Jan 2006 15:18:20 +0100] rev 18591
tuned EqSubst setup;
wenzelm [Fri, 06 Jan 2006 15:18:19 +0100] rev 18590
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
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;
wenzelm [Thu, 05 Jan 2006 22:29:59 +0100] rev 18588
tuned print_theorems_theory;
wenzelm [Thu, 05 Jan 2006 22:29:58 +0100] rev 18587
Toplevel.proof_position_of;
wenzelm [Thu, 05 Jan 2006 22:29:57 +0100] rev 18586
store_thm: transfer to current context, i.e. the target theory;
wenzelm [Thu, 05 Jan 2006 22:29:55 +0100] rev 18585
replaced swap by contrapos_np;
wenzelm [Thu, 05 Jan 2006 22:29:53 +0100] rev 18584
added setminus;
tuned;
wenzelm [Thu, 05 Jan 2006 17:16:40 +0100] rev 18583
proper handling of simultaneous goals and mutual rules;