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;