Mon, 06 Nov 2000 22:50:01 +0100 | wenzelm | Sign.typ_instance; | changeset | files |
Mon, 06 Nov 2000 22:49:16 +0100 | wenzelm | inductive_atomize, inductive_rulify; | changeset | files |
Mon, 06 Nov 2000 22:48:42 +0100 | wenzelm | * Isar/HOL: method 'induct' now handles non-atomic goals; as a | changeset | files |