| Mon, 15 Dec 2008 18:12:52 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:52:28 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 16:26:06 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 15 Nov 2006 20:50:23 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:16:59 +0100 |
wenzelm |
converted to 'inductive2';
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 14:28:47 +0200 |
haftmann |
hid succ, pred in Numeral.thy
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:12:03 +0100 |
wenzelm |
Abstract Natural Numbers with polymorphic recursion.
|
file |
diff |
annotate
|