src/ZF/ROOT.ML
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-11-21 clasohm 1995-11-21 main directory is now read by exit_use_dir, too; removed make_chart from ROOT.ML
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-04-25 lcp 1995-04-25 Now loads the theory "Let". Could add it to FOL, but this appears to be incompatible with CCL.
1994-12-16 lcp 1994-12-16 changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results.
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/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