src/ZF/Datatype.ML
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
2001-11-10 wenzelm 2001-11-10 use Tactic.prove;
2000-05-30 wenzelm 2000-05-30 cleaned up;
1999-10-04 wenzelm 1999-10-04 FOLogic.mk_conj;
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-13 paulson 1999-01-13 datatype package improvements
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1996-01-30 clasohm 1996-01-30 expanded tabs
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/Datatype/datatype_decl: supplies a SINGLE domain for the mutually recursive construction. This is [q]univ(A), which is closed under sum.
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-15 clasohm 1994-07-15 added thy_name to Datatype_Fun's parameter
1993-11-15 lcp 1993-11-15 changed all co- and co_ to co ZF/ex/llistfn: new coinduction example: flip ZF/ex/llist_eq: now uses standard pairs not qpairs
1993-10-22 lcp 1993-10-22 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works ZF/intr-elim/elim_rls: applied make_elim to succ_inject! ZF/fin: changed type_intrs in inductive def ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks, data_elims ZF/list: now uses datatype_intrs
1993-10-15 lcp 1993-10-15 ZF/ind-syntax/refl_thin: new ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD by dresolve_tac InlD,InrD and etac PartE
1993-09-16 clasohm 1993-09-16 Initial revision