| 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 |
| Mon, 12 Nov 2001 12:38:06 +0100 | paulson | Tidying necessitated by new simprules in equalities.ML | changeset | files |
| Mon, 12 Nov 2001 12:37:37 +0100 | paulson | conditional miniscoping equalities now made unconditional | changeset | files |
| Mon, 12 Nov 2001 10:56:38 +0100 | paulson | new-style numerals without leading #, along with generic 0 and 1 | changeset | files |