Mon, 12 Nov 2001 23:26:18 +0100 | wenzelm | induct_atomize: include atomize_conj (for mutual induction); | changeset | files |
Mon, 12 Nov 2001 23:25:25 +0100 | wenzelm | Isar: 'induct' proper support for mutual induction involving | changeset | files |
Mon, 12 Nov 2001 20:23:24 +0100 | wenzelm | proper handling of mutual rules (esp. for sets); | changeset | files |
Mon, 12 Nov 2001 20:22:51 +0100 | wenzelm | lemmas induct_atomize = atomize_conj ...; | changeset | files |
Mon, 12 Nov 2001 20:22:23 +0100 | wenzelm | val local_imp_def = thm "induct_implies_def"; | changeset | files |
Mon, 12 Nov 2001 12:38:40 +0100 | paulson | ZF/Induct,UNITY | changeset | files |