Fri, 25 Nov 2005 19:09:44 +0100 tuned induct proofs;
wenzelm [Fri, 25 Nov 2005 19:09:44 +0100] rev 18257
tuned induct proofs;
Fri, 25 Nov 2005 18:58:43 +0100 consume: unfold defs in all major prems;
wenzelm [Fri, 25 Nov 2005 18:58:43 +0100] rev 18256
consume: unfold defs in all major prems;
Fri, 25 Nov 2005 18:58:42 +0100 revert_skolem: fall back on Syntax.deskolem;
wenzelm [Fri, 25 Nov 2005 18:58:42 +0100] rev 18255
revert_skolem: fall back on Syntax.deskolem;
Fri, 25 Nov 2005 18:58:41 +0100 forall_conv ~1;
wenzelm [Fri, 25 Nov 2005 18:58:41 +0100] rev 18254
forall_conv ~1;
Fri, 25 Nov 2005 18:58:40 +0100 added dummy_pattern;
wenzelm [Fri, 25 Nov 2005 18:58:40 +0100] rev 18253
added dummy_pattern;
Fri, 25 Nov 2005 18:58:38 +0100 tuned names;
wenzelm [Fri, 25 Nov 2005 18:58:38 +0100] rev 18252
tuned names;
Fri, 25 Nov 2005 18:58:37 +0100 forall_conv: limit prefix;
wenzelm [Fri, 25 Nov 2005 18:58:37 +0100] rev 18251
forall_conv: limit prefix;
Fri, 25 Nov 2005 18:58:36 +0100 fix_tac: proper treatment of major premises in goal;
wenzelm [Fri, 25 Nov 2005 18:58:36 +0100] rev 18250
fix_tac: proper treatment of major premises in goal; export atomize/rulify interface; tuned;
Fri, 25 Nov 2005 18:58:35 +0100 removed obsolete dummy paragraphs;
wenzelm [Fri, 25 Nov 2005 18:58:35 +0100] rev 18249
removed obsolete dummy paragraphs;
Fri, 25 Nov 2005 18:58:34 +0100 tuned;
wenzelm [Fri, 25 Nov 2005 18:58:34 +0100] rev 18248
tuned;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip