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;
Thu, 05 Jan 2006 22:29:57 +0100 store_thm: transfer to current context, i.e. the target theory;
wenzelm [Thu, 05 Jan 2006 22:29:57 +0100] rev 18586
store_thm: transfer to current context, i.e. the target theory;
Thu, 05 Jan 2006 22:29:55 +0100 replaced swap by contrapos_np;
wenzelm [Thu, 05 Jan 2006 22:29:55 +0100] rev 18585
replaced swap by contrapos_np;
Thu, 05 Jan 2006 22:29:53 +0100 added setminus;
wenzelm [Thu, 05 Jan 2006 22:29:53 +0100] rev 18584
added setminus; tuned;
Thu, 05 Jan 2006 17:16:40 +0100 proper handling of simultaneous goals and mutual rules;
wenzelm [Thu, 05 Jan 2006 17:16:40 +0100] rev 18583
proper handling of simultaneous goals and mutual rules;
Thu, 05 Jan 2006 17:16:38 +0100 provide projections of induct_weak, induct_unsafe;
wenzelm [Thu, 05 Jan 2006 17:16:38 +0100] rev 18582
provide projections of induct_weak, induct_unsafe;
Thu, 05 Jan 2006 17:14:08 +0100 added strict_mutual_rule;
wenzelm [Thu, 05 Jan 2006 17:14:08 +0100] rev 18581
added strict_mutual_rule;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip