Tue, 16 Oct 2001 17:55:38 +0200 ignore typedef result;
wenzelm [Tue, 16 Oct 2001 17:55:38 +0200] rev 11806
ignore typedef result;
Tue, 16 Oct 2001 17:55:16 +0200 declare projected induction rules stemming from nested recursion;
wenzelm [Tue, 16 Oct 2001 17:55:16 +0200] rev 11805
declare projected induction rules stemming from nested recursion;
Tue, 16 Oct 2001 17:52:07 +0200 TypedefPackage.add_typedef_no_result;
wenzelm [Tue, 16 Oct 2001 17:52:07 +0200] rev 11804
TypedefPackage.add_typedef_no_result;
Tue, 16 Oct 2001 17:51:50 +0200 tuned;
wenzelm [Tue, 16 Oct 2001 17:51:50 +0200] rev 11803
tuned;
Tue, 16 Oct 2001 17:51:12 +0200 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
wenzelm [Tue, 16 Oct 2001 17:51:12 +0200] rev 11802
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);
Tue, 16 Oct 2001 17:25:44 +0200 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm [Tue, 16 Oct 2001 17:25:44 +0200] rev 11801
option -o FILE --output to FILE (ps, eps, pdf);
Tue, 16 Oct 2001 17:24:33 +0200 ISABELLE_EPSTOPDF="epstopdf";
wenzelm [Tue, 16 Oct 2001 17:24:33 +0200] rev 11800
ISABELLE_EPSTOPDF="epstopdf";
Tue, 16 Oct 2001 16:48:30 +0200 Font metrics used for batch mode layout (without X11 connection).
berghofe [Tue, 16 Oct 2001 16:48:30 +0200] rev 11799
Font metrics used for batch mode layout (without X11 connection).
Tue, 16 Oct 2001 16:47:54 +0200 Added support for batch mode layout (without X11 connection).
berghofe [Tue, 16 Oct 2001 16:47:54 +0200] rev 11798
Added support for batch mode layout (without X11 connection).
Tue, 16 Oct 2001 00:50:23 +0200 tuned;
wenzelm [Tue, 16 Oct 2001 00:50:23 +0200] rev 11797
tuned;
Tue, 16 Oct 2001 00:39:34 +0200 improved induct;
wenzelm [Tue, 16 Oct 2001 00:39:34 +0200] rev 11796
improved induct;
Tue, 16 Oct 2001 00:35:30 +0200 be more careful about token class markers;
wenzelm [Tue, 16 Oct 2001 00:35:30 +0200] rev 11795
be more careful about token class markers;
Tue, 16 Oct 2001 00:35:03 +0200 proper order of kind names;
wenzelm [Tue, 16 Oct 2001 00:35:03 +0200] rev 11794
proper order of kind names;
Tue, 16 Oct 2001 00:34:34 +0200 support impromptu terminology of cases parameters;
wenzelm [Tue, 16 Oct 2001 00:34:34 +0200] rev 11793
support impromptu terminology of cases parameters;
Tue, 16 Oct 2001 00:33:22 +0200 parser for underscore (actually a symbolic identifier!);
wenzelm [Tue, 16 Oct 2001 00:33:22 +0200] rev 11792
parser for underscore (actually a symbolic identifier!);
Tue, 16 Oct 2001 00:32:34 +0200 allow empty set/type name;
wenzelm [Tue, 16 Oct 2001 00:32:34 +0200] rev 11791
allow empty set/type name;
Tue, 16 Oct 2001 00:32:01 +0200 simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm [Tue, 16 Oct 2001 00:32:01 +0200] rev 11790
simplified resolveq_cases_tac for cases, separate version for induct; divinate instantiation of induct rules; tuned;
Tue, 16 Oct 2001 00:30:53 +0200 tuned;
wenzelm [Tue, 16 Oct 2001 00:30:53 +0200] rev 11789
tuned;
Mon, 15 Oct 2001 21:04:46 +0200 canonical 'cases'/'induct' rules for n-tuples (n=3..7)
kleing [Mon, 15 Oct 2001 21:04:46 +0200] rev 11788
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
Mon, 15 Oct 2001 21:04:32 +0200 canonical 'cases'/'induct' rules for n-tuples (n=3..7)
kleing [Mon, 15 Oct 2001 21:04:32 +0200] rev 11787
canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)
Mon, 15 Oct 2001 20:42:06 +0200 setsum syntax;
wenzelm [Mon, 15 Oct 2001 20:42:06 +0200] rev 11786
setsum syntax;
Mon, 15 Oct 2001 20:41:14 +0200 intro! and elim! rules;
wenzelm [Mon, 15 Oct 2001 20:41:14 +0200] rev 11785
intro! and elim! rules;
Mon, 15 Oct 2001 20:36:48 +0200 tuned NetRules;
wenzelm [Mon, 15 Oct 2001 20:36:48 +0200] rev 11784
tuned NetRules;
Mon, 15 Oct 2001 20:36:04 +0200 Tactic.orderlist;
wenzelm [Mon, 15 Oct 2001 20:36:04 +0200] rev 11783
Tactic.orderlist;
Mon, 15 Oct 2001 20:35:42 +0200 ObjectLogic.rulify;
wenzelm [Mon, 15 Oct 2001 20:35:42 +0200] rev 11782
ObjectLogic.rulify;
Mon, 15 Oct 2001 20:35:10 +0200 Tactic.rewrite_cterm;
wenzelm [Mon, 15 Oct 2001 20:35:10 +0200] rev 11781
Tactic.rewrite_cterm;
Mon, 15 Oct 2001 20:34:44 +0200 GPLed;
wenzelm [Mon, 15 Oct 2001 20:34:44 +0200] rev 11780
GPLed;
Mon, 15 Oct 2001 20:34:26 +0200 ring instead of ringS;
wenzelm [Mon, 15 Oct 2001 20:34:26 +0200] rev 11779
ring instead of ringS;
Mon, 15 Oct 2001 20:34:12 +0200 ring includes plus_ac0;
wenzelm [Mon, 15 Oct 2001 20:34:12 +0200] rev 11778
ring includes plus_ac0;
Mon, 15 Oct 2001 20:33:42 +0200 tuned;
wenzelm [Mon, 15 Oct 2001 20:33:42 +0200] rev 11777
tuned;
(0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip