1994-08-16 lcp 1994-08-16 ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
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
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1994-05-06 lcp 1994-05-06 renaming/removal of filenames to correct case
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files
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-11-04 clasohm 1993-11-04 renamed some files
1993-10-22 clasohm 1993-10-22 added -h 15000 for Poly/ML in Makefile, changed ROOT.ML for new Readthy
1993-10-11 clasohm 1993-10-11 renamed ordinal.* to ord.*
1993-10-06 clasohm 1993-10-06 changed "list-fn" to "listfn"
1993-09-30 lcp 1993-09-30 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
1993-09-17 lcp 1993-09-17 Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
1993-09-17 lcp 1993-09-17 test commit
1993-09-16 clasohm 1993-09-16 Initial revision