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;
Thu, 05 Jan 2006 17:14:07 +0100 RuleCases.strict_mutual_rule;
wenzelm [Thu, 05 Jan 2006 17:14:07 +0100] rev 18580
RuleCases.strict_mutual_rule; export internalize;
Thu, 05 Jan 2006 12:09:26 +0100 changed the name of the type "nOption" to "noption".
urbanc [Thu, 05 Jan 2006 12:09:26 +0100] rev 18579
changed the name of the type "nOption" to "noption".
Wed, 04 Jan 2006 20:20:25 +0100 added "fresh_singleton" lemma
urbanc [Wed, 04 Jan 2006 20:20:25 +0100] rev 18578
added "fresh_singleton" lemma
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip