src/ZF/ROOT.ML
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-02-11 wenzelm 2008-02-11 simultaneous use_thys;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2007-12-31 wenzelm 2007-12-31 removed obsolete banner;
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-05-31 wenzelm 2007-05-31 tuned ML setup;
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;
2005-10-19 wenzelm 2005-10-19 removed obsolete thy_syntax.ML;
2005-06-20 wenzelm 2005-06-20 removed obsolete print_depth;
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2002-01-11 wenzelm 2002-01-11 moved setmksimps to Main!
2001-12-19 paulson 2001-12-19 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
2001-11-09 wenzelm 2001-11-09 tuned;
2000-08-10 paulson 2000-08-10 installation of cancellation simprocs for the integers
2000-08-07 paulson 2000-08-07 instantiated Cancel_Numerals for "nat" in ZF
2000-06-30 paulson 2000-06-30 removal of batch-style proofs
2000-06-28 paulson 2000-06-28 simplified slightly by using dependencies better in theories
2000-05-05 wenzelm 2000-05-05 removed Pure/section_utils.ML;
2000-01-13 paulson 2000-01-13 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed from directory AC
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1999-02-08 wenzelm 1999-02-08 ~~;
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-08 paulson 1999-01-08 removal of DO_GOAL
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-06 paulson 1999-01-06 induct_tac and exhaust_tac
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-09-22 paulson 1998-09-22 tidying
1998-09-18 paulson 1998-09-18 leaves subgoal package empty
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-11-20 wenzelm 1997-11-20 $ISABELLE_HOME/src;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
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