Mon, 05 Aug 2002 21:17:04 +0200 | wenzelm | tuned; | changeset | files |
Mon, 05 Aug 2002 21:16:36 +0200 | wenzelm | special syntax for index "1" (plain numeral hidden by "1" symbol in HOL); | changeset | files |
Mon, 05 Aug 2002 14:35:33 +0200 | berghofe | Removed theory NatDef. | changeset | files |
Mon, 05 Aug 2002 14:32:56 +0200 | berghofe | Replaced nat_ind_tac by induct_tac. | changeset | files |
Mon, 05 Aug 2002 14:30:06 +0200 | berghofe | Removed proof of Suc_le_D (already proved in Nat.thy). | changeset | files |
Mon, 05 Aug 2002 14:29:20 +0200 | berghofe | Removed reference to theory NatDef. | changeset | files |