| Mon, 14 Jul 2008 11:04:42 +0200 | haftmann | unified curried gcd, lcm, zgcd, zlcm | file | diff | annotate |
| Thu, 26 Jun 2008 10:06:53 +0200 | haftmann | dropped recdef | file | diff | annotate |
| Wed, 23 Nov 2005 22:26:13 +0100 | wenzelm | tuned induction proofs; | 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 |
| Fri, 14 Jan 2005 12:00:27 +0100 | nipkow | made diff_less a simp rule | file | diff | annotate |
| Tue, 16 Oct 2001 17:58:13 +0200 | wenzelm | tuned induction 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 Aug 2001 13:43:24 +0200 | nipkow | turned translation for 1::nat into def. | file | diff | annotate |
| Mon, 06 Nov 2000 22:56:07 +0100 | wenzelm | improved: 'induct' handle non-atomic goals; | file | diff | annotate |
| Sun, 17 Sep 2000 22:19:02 +0200 | wenzelm | isar-strip-terminators; | file | diff | annotate |
| Wed, 06 Sep 2000 08:04:41 +0200 | nipkow | less_induct -> nat_less_induct | file | diff | annotate |
| Mon, 04 Sep 2000 10:26:34 +0200 | paulson | minor fixes for new version of Primes.thy | file | diff | annotate |
| Sat, 19 Aug 2000 12:44:39 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 23 May 2000 18:06:22 +0200 | paulson | added type constraint ::nat because 0 is now overloaded | file | diff | annotate |
| Fri, 05 May 2000 22:30:14 +0200 | wenzelm | adapted to new arithmetic simprocs; | file | diff | annotate |
| Thu, 30 Mar 2000 19:45:51 +0200 | nipkow | recdef.rules -> recdef.simps | file | diff | annotate |
| Sun, 27 Feb 2000 15:25:31 +0100 | wenzelm | even better induct setup; | file | diff | annotate |
| Tue, 22 Feb 2000 21:50:02 +0100 | wenzelm | tuned "induct" syntax; | file | diff | annotate |
| Tue, 07 Dec 1999 17:14:49 +0100 | wenzelm | tuned; | file | diff | annotate |
| Tue, 07 Dec 1999 12:13:09 +0100 | wenzelm | tuned; | file | diff | annotate |