| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 12:29:57 +0100 |
haftmann |
removed includes
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:15:48 +0100 |
haftmann |
added rudimentary code generation
|
file |
diff |
annotate
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| 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
|