src/ZF/Datatype.thy
2007-06-19 wenzelm 2007-06-19 BalancedTree;
2007-04-26 wenzelm 2007-04-26 removed lagacy ML files;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-07-09 paulson 2002-07-09 better document preparation
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
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-04-02 paulson 1997-04-02 Now a non-trivial theory so that require_thy can find it
1994-12-19 lcp 1994-12-19 removed quotes around "Inductive"
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
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files