| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 08:44:04 +0200 |
paulson |
addition of the GREATEST quantifier
|
file |
diff |
annotate
|
| Thu, 15 Feb 2001 16:12:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2001 16:01:22 +0100 |
oheimb |
Ord.thy/.ML converted to Isar
|
file |
diff |
annotate
|
| Mon, 13 Nov 2000 08:53:21 +0100 |
nipkow |
Removed > and >= again.
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 16:26:44 +0100 |
nipkow |
new: > and >=
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 08:00:34 +0200 |
nipkow |
<= -> \<le>
|
file |
diff |
annotate
|
| Thu, 18 May 2000 11:43:57 +0200 |
wenzelm |
fewer consts declared as global;
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 20:49:02 +0200 |
wenzelm |
proper bootstrap of HOL theory and packages;
|
file |
diff |
annotate
|
| Tue, 17 Aug 1999 22:13:23 +0200 |
wenzelm |
replaced HOL_quantifiers flag by "HOL" print mode;
|
file |
diff |
annotate
|
| Tue, 29 Jun 1999 11:58:21 +0200 |
nipkow |
Bad translation fixed.
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 10:44:42 +0200 |
wenzelm |
hol_setup, simpdata_setup;
|
file |
diff |
annotate
|
| Thu, 18 Mar 1999 16:42:34 +0100 |
nipkow |
New bounded quantifier syntax: !x<i. P etc
|
file |
diff |
annotate
|
| Tue, 24 Nov 1998 12:03:09 +0100 |
wenzelm |
setup Blast.setup;
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 11:12:59 +0100 |
wenzelm |
Classical.setup, attrib_setup;
|
file |
diff |
annotate
|
| 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
|