src/ZF/Inductive.ML
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1997-12-03 paulson 1997-12-03 Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1996-05-08 paulson 1996-05-08 Modified to use new functor signatures
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-22 paulson 1995-12-22 Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule. intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of generating a new one. Inductive defs no longer export sumprod_free_SEs ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store. Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items no longer exported. mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
1995-05-03 lcp 1995-05-03 Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.
1994-12-16 lcp 1994-12-16 Defines ZF theory sections (inductive, datatype) at the start/ Moved theory section code here from Inductive.ML and Datatype.ML
1994-11-24 lcp 1994-11-24 ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually recursive datatypes, especially with monotone operators Inductive_Fun,CoInductive_Fun: deleted as obsolete inductive_decl: now reads a SINGLE domain for the mutually recursive construction. This could be a sum, perhaps not! CONCRETE SYNTAX has changed too (but there are no examples of this to change).
1994-08-25 lcp 1994-08-25 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils