Mon, 10 Dec 2007 11:24:12 +0100 |
haftmann |
switched import from Main to List
|
file |
diff |
annotate
|
Fri, 05 Oct 2007 23:04:14 +0200 |
wenzelm |
tuned proofs (via polymorphic taking'');
|
file |
diff |
annotate
|
Fri, 05 Oct 2007 22:00:13 +0200 |
wenzelm |
coinduct: instantiation refers to suffix of main prop (major premise or conclusion);
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:28:13 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
Tue, 24 Apr 2007 15:15:52 +0200 |
berghofe |
Adapted to new parse translation for case expressions.
|
file |
diff |
annotate
|
Tue, 27 Feb 2007 00:33:49 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Sun, 01 Oct 2006 22:19:23 +0200 |
wenzelm |
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
|
file |
diff |
annotate
|
Sat, 30 Sep 2006 21:39:27 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Thu, 28 Sep 2006 23:42:43 +0200 |
wenzelm |
fixed translations: CONST;
|
file |
diff |
annotate
|
Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|
Sat, 21 Jan 2006 23:02:21 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Tue, 13 Dec 2005 19:32:36 +0100 |
wenzelm |
Potentially infinite lists as greatest fixed-point.
|
file |
diff |
annotate
|