wenzelm [Wed, 23 Nov 2005 18:52:02 +0100] rev 18235
(co)induct: taking;
induct set: proper treatment of defs;
wenzelm [Wed, 23 Nov 2005 18:52:01 +0100] rev 18234
RuleCases.case_conclusion;
wenzelm [Wed, 23 Nov 2005 18:52:00 +0100] rev 18233
tuned;
wenzelm [Wed, 23 Nov 2005 18:51:59 +0100] rev 18232
added case_conclusion attribute;
added coinduct method/attribute;
induct method: definsts/fixing/taking;
tuned;
haftmann [Wed, 23 Nov 2005 17:16:42 +0100] rev 18231
improved failure tracking
wenzelm [Tue, 22 Nov 2005 19:37:36 +0100] rev 18230
Datatype_Universe: hide base names only;
wenzelm [Tue, 22 Nov 2005 19:34:50 +0100] rev 18229
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
added consume rule;
support named case conclusions;
tuned interfaces;
wenzelm [Tue, 22 Nov 2005 19:34:48 +0100] rev 18228
cases_tactic;