Tue, 13 Nov 2001 22:25:59 +0100 * ZF: new-style theory commands 'inductive', 'inductive_cases', and
wenzelm [Tue, 13 Nov 2001 22:25:59 +0100] rev 12177
* ZF: new-style theory commands 'inductive', 'inductive_cases', and methods 'ind_cases', 'induct_tac', 'case_tac';
Tue, 13 Nov 2001 22:24:28 +0100 ZF specific keywords;
wenzelm [Tue, 13 Nov 2001 22:24:28 +0100] rev 12176
ZF specific keywords;
Tue, 13 Nov 2001 22:20:51 +0100 rearranged inductive package for Isar;
wenzelm [Tue, 13 Nov 2001 22:20:51 +0100] rev 12175
rearranged inductive package for Isar;
Tue, 13 Nov 2001 22:20:15 +0100 Generic inductive cases facility for (co)inductive definitions.
wenzelm [Tue, 13 Nov 2001 22:20:15 +0100] rev 12174
Generic inductive cases facility for (co)inductive definitions.
Tue, 13 Nov 2001 22:19:37 +0100 converted;
wenzelm [Tue, 13 Nov 2001 22:19:37 +0100] rev 12173
converted;
Tue, 13 Nov 2001 22:18:46 +0100 tuned;
wenzelm [Tue, 13 Nov 2001 22:18:46 +0100] rev 12172
tuned;
Tue, 13 Nov 2001 22:18:03 +0100 tuned inductions;
wenzelm [Tue, 13 Nov 2001 22:18:03 +0100] rev 12171
tuned inductions;
Tue, 13 Nov 2001 17:51:03 +0100 prove: Envir.beta_norm;
wenzelm [Tue, 13 Nov 2001 17:51:03 +0100] rev 12170
prove: Envir.beta_norm;
Tue, 13 Nov 2001 16:12:25 +0100 new SList theory from Bu Wolff
paulson [Tue, 13 Nov 2001 16:12:25 +0100] rev 12169
new SList theory from Bu Wolff
Mon, 12 Nov 2001 23:30:16 +0100 induct: rule_versions produces localized variants;
wenzelm [Mon, 12 Nov 2001 23:30:16 +0100] rev 12168
induct: rule_versions produces localized variants;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip