wenzelm [Fri, 06 Jan 2006 18:18:12 +0100] rev 18594
obsolete, reuse mk_rews of local simpset;
wenzelm [Fri, 06 Jan 2006 15:18:22 +0100] rev 18593
Toplevel.theory_to_proof;
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;