| Wed, 13 Jun 2007 18:30:11 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
| Wed, 07 Feb 2007 17:46:03 +0100 | berghofe | Adapted to changes in Finite_Set theory. | file | diff | annotate |
| Wed, 23 Nov 2005 22:26:13 +0100 | wenzelm | tuned induction proofs; | file | diff | annotate |
| Wed, 16 Nov 2005 17:50:35 +0100 | wenzelm | tuned; | file | diff | annotate |
| Thu, 10 Nov 2005 21:14:05 +0100 | wenzelm | tuned proofs; | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Thu, 30 May 2002 10:12:52 +0200 | nipkow | Modifications due to enhanced linear arithmetic. | file | diff | annotate |
| Tue, 30 Oct 2001 17:37:25 +0100 | wenzelm | tuned induct proofs; | file | diff | annotate |
| Sat, 06 Oct 2001 00:02:46 +0200 | wenzelm | * sane numerals (stage 2): plain "num" syntax (removed "#"); | file | diff | annotate |
| Fri, 05 Oct 2001 21:52:39 +0200 | wenzelm | sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, | file | diff | annotate |
| Mon, 06 Nov 2000 22:56:07 +0100 | wenzelm | improved: 'induct' handle non-atomic goals; | file | diff | annotate |
| Fri, 03 Nov 2000 21:33:53 +0100 | wenzelm | adapted "obtain" proofs; | file | diff | annotate |
| Sun, 17 Sep 2000 22:19:02 +0200 | wenzelm | isar-strip-terminators; | file | diff | annotate |
| Tue, 12 Sep 2000 22:13:23 +0200 | wenzelm | renamed atts: rulify to rule_format, elimify to elim_format; | file | diff | annotate |
| Thu, 07 Sep 2000 21:10:11 +0200 | wenzelm | updated attribute names; | file | diff | annotate |
| Sat, 19 Aug 2000 12:44:39 +0200 | wenzelm | tuned; | file | diff | annotate |
| Thu, 17 Aug 2000 10:34:11 +0200 | wenzelm | 'symmetric' attribute; | file | diff | annotate |
| Mon, 14 Aug 2000 18:13:14 +0200 | wenzelm | intros; | file | diff | annotate |
| Sun, 30 Jul 2000 13:03:49 +0200 | wenzelm | adapted obtain; | file | diff | annotate |
| Fri, 05 May 2000 22:30:14 +0200 | wenzelm | adapted to new arithmetic simprocs; | file | diff | annotate |
| Thu, 13 Apr 2000 15:01:50 +0200 | nipkow | Times -> <*> | file | diff | annotate |
| Wed, 05 Apr 2000 21:06:37 +0200 | wenzelm | fixed goal selection; | file | diff | annotate |
| Thu, 24 Feb 2000 21:33:32 +0100 | wenzelm | simplified induct method; | file | diff | annotate |
| Tue, 22 Feb 2000 21:50:02 +0100 | wenzelm | tuned "induct" syntax; | file | diff | annotate |
| Thu, 28 Oct 1999 19:57:34 +0200 | wenzelm | improved presentation; | file | diff | annotate |
| Fri, 15 Oct 1999 16:44:37 +0200 | wenzelm | improved presentation; | file | diff | annotate |
| Fri, 08 Oct 1999 15:09:14 +0200 | wenzelm | improved presentation; | file | diff | annotate |
| Wed, 06 Oct 1999 18:50:51 +0200 | wenzelm | improved presentation; | file | diff | annotate |
| Tue, 21 Sep 1999 17:30:55 +0200 | wenzelm | accomodate refined facts handling; | file | diff | annotate |
| Sat, 04 Sep 1999 21:13:01 +0200 | wenzelm | replaced ?? by ?; | file | diff | annotate |
| Fri, 03 Sep 1999 14:21:59 +0200 | wenzelm | from hyp; | file | diff | annotate |
| Wed, 01 Sep 1999 21:35:39 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 30 Aug 1999 11:13:27 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sun, 29 Aug 1999 17:52:44 +0200 | wenzelm | added Isar_examples/MutilatedCheckerboard.thy; | file | diff | annotate |
| Sun, 29 Aug 1999 17:47:26 +0200 | wenzelm | The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil; | file | diff | annotate |