| Fri, 02 Dec 1994 16:13:34 +0100 |
nipkow |
Moved the old List to ex and replaced it by one defined via
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 13:34:33 +0100 |
nipkow |
Removed obsolete induction package
|
file |
diff |
annotate
|
| Wed, 23 Nov 1994 10:37:27 +0100 |
wenzelm |
moved remaining thy syntax stuff to thy_syntax.ML;
|
file |
diff |
annotate
|
| Tue, 08 Nov 1994 11:21:33 +0100 |
lcp |
HOL/ROOT/HOL_dup_cs: removed as obsolete
|
file |
diff |
annotate
|
| Fri, 04 Nov 1994 14:19:30 +0100 |
wenzelm |
rearranged theory section stuff;
|
file |
diff |
annotate
|
| Wed, 28 Sep 1994 12:39:32 +0100 |
nipkow |
moved LList* to ex
|
file |
diff |
annotate
|
| Tue, 30 Aug 1994 10:04:49 +0200 |
nipkow |
New version of datatype.ML with primrec (Norbert).
|
file |
diff |
annotate
|
| Thu, 25 Aug 1994 11:01:45 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 11:25:16 +0200 |
lcp |
HOL/Makefile, ROOT: updated for new .thy files
|
file |
diff |
annotate
|
| Sat, 13 Aug 1994 16:33:53 +0200 |
nipkow |
Added primitive recursive functions (Norbert Voelker's code) to the datatype
|
file |
diff |
annotate
|
| Mon, 20 Jun 1994 12:05:03 +0200 |
nipkow |
Datatype -> Datatype.ML
|
file |
diff |
annotate
|
| Fri, 17 Jun 1994 14:15:38 +0200 |
clasohm |
datatypes must now be defined using a thy file section
|
file |
diff |
annotate
|
| Thu, 19 May 1994 17:07:19 +0200 |
wenzelm |
thy reader now initialised by init_thy_reader();
|
file |
diff |
annotate
|
| Fri, 18 Mar 1994 20:32:18 +0100 |
nipkow |
added use_thy"Datatype"
|
file |
diff |
annotate
|
| Tue, 04 Jan 1994 18:33:20 +0100 |
nipkow |
shortened use_thy section taking advantage of dependencies
|
file |
diff |
annotate
|
| Tue, 16 Nov 1993 14:14:22 +0100 |
clasohm |
changed use_thy's parameter to exact theory name
|
file |
diff |
annotate
|
| Fri, 22 Oct 1993 13:36:28 +0100 |
clasohm |
changes for new Readthy
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|