| Tue, 06 Aug 2002 11:19:52 +0200 | wenzelm | predefined locales "var" and "struct" (useful for sharing parameters); | changeset | files |
| Tue, 06 Aug 2002 11:19:00 +0200 | wenzelm | * Pure: predefined locales "var" and "struct" are useful for sharing | changeset | files |
| Mon, 05 Aug 2002 21:17:45 +0200 | wenzelm | protect simplifier operation against spurious exceptions from simprocs; | changeset | files |
| 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 |