| Tue, 28 Feb 1995 10:52:55 +0100 |
lcp |
No longer calls maketest; instead, the Makefile writes the file
|
file |
diff |
annotate
|
| Fri, 03 Feb 1995 16:19:45 +0100 |
nipkow |
Added Markus Wenzel's string representation.
|
file |
diff |
annotate
|
| Fri, 02 Dec 1994 16:09:49 +0100 |
nipkow |
Moved HOL/List to HOL/ex/SList (strict list).
|
file |
diff |
annotate
|
| Wed, 28 Sep 1994 12:39:32 +0100 |
nipkow |
moved LList* to ex
|
file |
diff |
annotate
|
| Tue, 30 Aug 1994 10:05:46 +0200 |
nipkow |
Updated PL to PropLog using Larrys ind. defs.
|
file |
diff |
annotate
|
| Thu, 25 Aug 1994 10:47:33 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
file |
diff |
annotate
|
| Sun, 27 Mar 1994 16:43:06 +0200 |
nipkow |
Added some sums.
|
file |
diff |
annotate
|
| Wed, 23 Feb 1994 10:05:35 +0100 |
nipkow |
some more sorting algorithms
|
file |
diff |
annotate
|
| Mon, 24 Jan 1994 15:59:44 +0100 |
nipkow |
added qsort
|
file |
diff |
annotate
|
| Tue, 09 Nov 1993 13:30:13 +0100 |
clasohm |
renamed meson-test.ML to mesontest.ML,
|
file |
diff |
annotate
|
| Tue, 09 Nov 1993 11:08:13 +0100 |
lcp |
co-induction example courtesy Jacob Frost
|
file |
diff |
annotate
|
| Sun, 17 Oct 1993 17:33:40 +0100 |
clasohm |
renamed: hol-rec.* to rec.*, lex-prod.* to lexprod.*, prop-log.* to pl.*
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|