| Mon, 14 Aug 2000 18:43:57 +0200 | wenzelm | updated command termination issue; | changeset | files |
| Mon, 14 Aug 2000 18:43:30 +0200 | wenzelm | some more refs; | changeset | files |
| Mon, 14 Aug 2000 18:42:57 +0200 | wenzelm | Aspinall:2000:eProof; | changeset | files |
| Mon, 14 Aug 2000 18:14:54 +0200 | wenzelm | raplaced "intrs" by "intrs" (new-style only); | changeset | files |
| Mon, 14 Aug 2000 18:13:42 +0200 | wenzelm | cases: support multiple insts; | changeset | files |
| Mon, 14 Aug 2000 18:13:14 +0200 | wenzelm | intros; | changeset | files |
| Mon, 14 Aug 2000 18:08:26 +0200 | kleing | added MicroJava/BV/StepMono.thy, | changeset | files |
| Mon, 14 Aug 2000 18:03:19 +0200 | kleing | Convert.thy now in Isar, tuned | changeset | files |
| Mon, 14 Aug 2000 14:57:29 +0200 | wenzelm | tuned names; | changeset | files |
| Mon, 14 Aug 2000 14:53:47 +0200 | wenzelm | added hypsubst; | changeset | files |
| Mon, 14 Aug 2000 14:53:26 +0200 | wenzelm | added "fastsimp"; | changeset | files |
| Mon, 14 Aug 2000 14:51:51 +0200 | wenzelm | added declare_theorems(_i); | changeset | files |
| Mon, 14 Aug 2000 14:50:53 +0200 | wenzelm | added "declare" command; | changeset | files |
| Mon, 14 Aug 2000 14:50:32 +0200 | wenzelm | added thy_script kind; | changeset | files |
| Mon, 14 Aug 2000 14:50:11 +0200 | wenzelm | tuned msg; | changeset | files |
| Mon, 14 Aug 2000 14:49:49 +0200 | wenzelm | use_let: exclude 'val'; | changeset | files |
| Mon, 14 Aug 2000 14:48:07 +0200 | wenzelm | fixed document preparation; | changeset | files |
| Sat, 12 Aug 2000 21:42:51 +0200 | paulson | documented the integers and updated section on nat arithmetic | changeset | files |
| Sat, 12 Aug 2000 21:42:12 +0200 | paulson | some ad-hoc simprules for div and mod to reduce the | changeset | files |
| Sat, 12 Aug 2000 21:41:42 +0200 | paulson | deleted needless rules | changeset | files |
| Fri, 11 Aug 2000 14:53:48 +0200 | kleing | added bind_thm for widen_RefT etc. | changeset | files |
| Fri, 11 Aug 2000 14:52:52 +0200 | kleing | tuned | changeset | files |
| Fri, 11 Aug 2000 14:52:39 +0200 | kleing | added LBV | changeset | files |
| Fri, 11 Aug 2000 13:27:17 +0200 | paulson | new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers | changeset | files |
| Fri, 11 Aug 2000 13:26:40 +0200 | paulson | ZF arith | changeset | files |
| Fri, 11 Aug 2000 10:34:02 +0200 | paulson | interim working version: more improvements to the integers | changeset | files |
| Thu, 10 Aug 2000 14:55:21 +0200 | berghofe | Equations that are added to the simpset now have proper names. | changeset | files |
| Thu, 10 Aug 2000 11:39:53 +0200 | paulson | new structure field "add" for CombineNumerals | changeset | files |
| Thu, 10 Aug 2000 11:33:40 +0200 | paulson | the "nocheck" versions of goal functions now standardize their result | changeset | files |
| Thu, 10 Aug 2000 11:30:39 +0200 | paulson | tidied | changeset | files |