wenzelm [Tue, 16 Oct 2001 00:50:23 +0200] rev 11797
tuned;
wenzelm [Tue, 16 Oct 2001 00:39:34 +0200] rev 11796
improved induct;
wenzelm [Tue, 16 Oct 2001 00:35:30 +0200] rev 11795
be more careful about token class markers;
wenzelm [Tue, 16 Oct 2001 00:35:03 +0200] rev 11794
proper order of kind names;
wenzelm [Tue, 16 Oct 2001 00:34:34 +0200] rev 11793
support impromptu terminology of cases parameters;
wenzelm [Tue, 16 Oct 2001 00:33:22 +0200] rev 11792
parser for underscore (actually a symbolic identifier!);
wenzelm [Tue, 16 Oct 2001 00:32:34 +0200] rev 11791
allow empty set/type name;
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;
wenzelm [Tue, 16 Oct 2001 00:30:53 +0200] rev 11789
tuned;
kleing [Mon, 15 Oct 2001 21:04:46 +0200] rev 11788
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)
wenzelm [Mon, 15 Oct 2001 20:42:06 +0200] rev 11786
setsum syntax;
wenzelm [Mon, 15 Oct 2001 20:41:14 +0200] rev 11785
intro! and elim! rules;
wenzelm [Mon, 15 Oct 2001 20:36:48 +0200] rev 11784
tuned NetRules;