src/ZF/Inductive.thy
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-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-06-29 paulson 2002-06-29 conversion of many files to Isar format
2001-12-05 wenzelm 2001-12-05 tuned declarations;
2001-11-15 wenzelm 2001-11-15 setup DatatypeTactics.setup;
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
2000-08-01 paulson 2000-08-01 natify, a coercion to reduce the number of type constraints in arithmetic
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 added true theory dependencies
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