| 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
|