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 |
Mon, 12 Nov 2001 10:44:55 +0100 | berghofe | congc now returns None if congruence rule has no effect. | changeset | files |