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)
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip