| Tue, 12 Jan 1999 15:17:37 +0100 |
wenzelm |
eliminated global/local names;
|
file |
diff |
annotate
|
| Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 17:42:39 +0200 |
wenzelm |
(co) inductive / datatype package adapted to qualified names;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 11:57:52 +0200 |
wenzelm |
use ThySyn.add_syntax;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 00:47:20 +0200 |
berghofe |
Replaced "init_thy_reader" by "set_parser".
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:16:12 +0200 |
paulson |
A slight simplification of optstring
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Thu, 28 Dec 1995 12:37:57 +0100 |
paulson |
Reduced indentation; no change in function
|
file |
diff |
annotate
|
| Fri, 22 Dec 1995 11:09:28 +0100 |
paulson |
Improving space efficiency of inductive/datatype definitions.
|
file |
diff |
annotate
|
| Fri, 16 Dec 1994 17:36:50 +0100 |
lcp |
Defines ZF theory sections (inductive, datatype) at the start/
|
file |
diff |
annotate
|