src/ZF/InfDatatype.ML
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-16 wenzelm 1997-10-16 transfer InfDatatype.thy Limit_VfromE;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-01-30 clasohm 1996-01-30 expanded tabs
1994-12-16 lcp 1994-12-16 Added Limit_csucc from CardinalArith Moved all theorems concerning FINITE functions to Univ.ML and deleted the declaration val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
1994-12-08 lcp 1994-12-08 UN_upper_cardinal: updated to refer to Card_le_imp_lepoll and lepoll_imp_Card_le
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-11-03 lcp 1994-11-03 ZF/InfDatatype/fun_Vcsucc: removed use of PiE
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-15 lcp 1994-08-15 ZF/InfDatatype: simplified, extended results for infinite branching
1994-08-12 lcp 1994-08-12 for infinite datatypes with arbitrary index sets
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-27 lcp 1994-07-27 Addition of infinite branching datatypes