| Mon, 22 Aug 1994 11:02:35 +0200 |
lcp |
changed defn to def
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 16:18:44 +0200 |
wenzelm |
replaced add_defns_i by add_defs_i;
|
file |
diff |
annotate
|
| Tue, 16 Aug 1994 09:57:51 +0200 |
nipkow |
allow long_id for reference to type in primrec.
|
file |
diff |
annotate
|
| Mon, 15 Aug 1994 15:20:34 +0200 |
nipkow |
Cleaned up code.
|
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
|
| Fri, 15 Jul 1994 14:04:28 +0200 |
nipkow |
Lots of simplifications
|
file |
diff |
annotate
|
| Fri, 08 Jul 1994 17:22:58 +0200 |
nipkow |
Hidden dtK and Impossible with a "local" clause
|
file |
diff |
annotate
|
| Fri, 08 Jul 1994 12:01:55 +0200 |
clasohm |
added mixfix annotations to constructor declarations
|
file |
diff |
annotate
|
| Mon, 20 Jun 1994 14:52:40 +0200 |
clasohm |
added prefix to name of induct axiom
|
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
|
| Tue, 22 Mar 1994 19:54:55 +0100 |
nipkow |
new field "simps" added
|
file |
diff |
annotate
|
| Fri, 18 Mar 1994 20:33:32 +0100 |
nipkow |
ML-like datatype decalaration facility. Axiomatic.
|
file |
diff |
annotate
|