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