| Fri, 09 Nov 2001 22:53:41 +0100 |
wenzelm |
support co/inductive definitions in new-style theories;
|
file |
diff |
annotate
|
| Fri, 13 Oct 2000 11:15:56 +0200 |
paulson |
renamed fp_Tarski to fp_unfold
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 15:17:37 +0100 |
wenzelm |
eliminated global/local names;
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 10:52:17 +0100 |
paulson |
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
|
file |
diff |
annotate
|
| Wed, 08 May 1996 17:59:21 +0200 |
paulson |
Modified to use new functor signatures
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 22 Dec 1995 11:09:28 +0100 |
paulson |
Improving space efficiency of inductive/datatype definitions.
|
file |
diff |
annotate
|
| Wed, 03 May 1995 14:17:01 +0200 |
lcp |
Changed to use split instead of fsplit. The weakening of fsplitE appears not
|
file |
diff |
annotate
|
| Fri, 16 Dec 1994 17:46:02 +0100 |
lcp |
Defines ZF theory sections (inductive, datatype) at the start/
|
file |
diff |
annotate
|
| Thu, 24 Nov 1994 00:32:12 +0100 |
lcp |
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
|
file |
diff |
annotate
|
| Thu, 25 Aug 1994 12:09:21 +0200 |
lcp |
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
|
file |
diff |
annotate
|