wenzelm [Tue, 13 Nov 2001 22:20:51 +0100] rev 12175
rearranged inductive package for Isar;
wenzelm [Tue, 13 Nov 2001 22:20:15 +0100] rev 12174
Generic inductive cases facility for (co)inductive definitions.
wenzelm [Tue, 13 Nov 2001 22:19:37 +0100] rev 12173
converted;
wenzelm [Tue, 13 Nov 2001 22:18:46 +0100] rev 12172
tuned;
wenzelm [Tue, 13 Nov 2001 22:18:03 +0100] rev 12171
tuned inductions;
wenzelm [Tue, 13 Nov 2001 17:51:03 +0100] rev 12170
prove: Envir.beta_norm;
paulson [Tue, 13 Nov 2001 16:12:25 +0100] rev 12169
new SList theory from Bu Wolff
wenzelm [Mon, 12 Nov 2001 23:30:16 +0100] rev 12168
induct: rule_versions produces localized variants;
wenzelm [Mon, 12 Nov 2001 23:28:49 +0100] rev 12167
empty rule_context for multiple goals;
wenzelm [Mon, 12 Nov 2001 23:28:15 +0100] rev 12166
added empty;
wenzelm [Mon, 12 Nov 2001 23:27:04 +0100] rev 12165
mutual rules declared as ``consumes 0'';
wenzelm [Mon, 12 Nov 2001 23:26:18 +0100] rev 12164
induct_atomize: include atomize_conj (for mutual induction);
wenzelm [Mon, 12 Nov 2001 23:25:25 +0100] rev 12163
Isar: 'induct' proper support for mutual induction involving
non-atomic rule statements;
Isar/Pure: support multiple simultaneous goal statements;
wenzelm [Mon, 12 Nov 2001 20:23:24 +0100] rev 12162
proper handling of mutual rules (esp. for sets);
wenzelm [Mon, 12 Nov 2001 20:22:51 +0100] rev 12161
lemmas induct_atomize = atomize_conj ...;
val local_imp_def = thm "induct_implies_def";