isabelle: Changelog

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;

wenzelm [Mon, 15 Oct 2001 20:36:04 +0200] rev 11783

Tactic.orderlist;

isabelle