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
|