src/ZF/Finite.thy
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.
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1995-06-22 clasohm 1995-06-22 removed \...\ inside strings
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-16 lcp 1994-08-16 ZF/Finite: added the finite function space, A-||>B ZF/InfDatatype: added rules for the above
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections