| Fri, 20 Feb 1998 17:56:39 +0100 |
nipkow |
Congruence rules use == in premises now.
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 11:25:39 +0200 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|
| Thu, 09 Oct 1997 15:03:06 +0200 |
wenzelm |
fixed infix syntax;
|
file |
diff |
annotate
|
| Thu, 08 May 1997 11:44:59 +0200 |
nipkow |
Modified def of Least, which, as Markus correctly complained, looked like
|
file |
diff |
annotate
|
| Fri, 14 Feb 1997 15:32:00 +0100 |
wenzelm |
fixed comment;
|
file |
diff |
annotate
|
| Wed, 12 Feb 1997 18:53:59 +0100 |
nipkow |
New class "order" and accompanying changes.
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 16:48:19 +0100 |
wenzelm |
fixed comment;
|
file |
diff |
annotate
|
| Mon, 23 Sep 1996 17:47:49 +0200 |
paulson |
New infix syntax: breaks line BEFORE operator
|
file |
diff |
annotate
|
| Wed, 29 Nov 1995 16:44:59 +0100 |
clasohm |
removed quotes from types in consts and syntax sections
|
file |
diff |
annotate
|
| Mon, 20 Mar 1995 15:35:28 +0100 |
clasohm |
changed syntax of "if"
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|