src/ZF/thy_syntax.ML
1999-05-12 wenzelm 1999-05-12 strip_quotes replaced by unenclose;
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-12 wenzelm 1999-01-12 eliminated global/local names;
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1997-10-17 wenzelm 1997-10-17 (co) inductive / datatype package adapted to qualified names;
1997-08-06 wenzelm 1997-08-06 use ThySyn.add_syntax;
1997-08-06 berghofe 1997-08-06 Replaced "init_thy_reader" by "set_parser".
1997-06-05 paulson 1997-06-05 A slight simplification of optstring
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-28 paulson 1995-12-28 Reduced indentation; no change in function
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.
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