1996-02-10 clasohm 1996-02-10 make_html now only remains set if MAKE_HTML=true
1995-11-21 clasohm 1995-11-21 main directory is now read by exit_use_dir, too; removed make_chart from ROOT.ML
1995-11-21 clasohm 1995-11-21 replaced exit_use by exit_use_dir for subdirectories
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-10-16 paulson 1995-10-16 Added the new Limit.{thy,ML} example
1995-07-26 lcp 1995-07-26 Now includes all the AC files
1995-04-14 lcp 1995-04-14 Now builds Resid as a test
1995-04-06 lcp 1995-04-06 Added Id: line
1995-03-31 lcp 1995-03-31 Simplified using pattern replacements. Added the AC example.
1995-03-15 lcp 1995-03-15 Now calls exit_use instead of use, for prompt failure if errors are detected.
1995-02-28 lcp 1995-02-28 Re-organised to perform the tests independently. Now test is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to refer to the right command for running the object-logic. Uses "suffix substitution" to shorten macro definitions.
1994-12-16 lcp 1994-12-16 added thy_syntax.ML
1994-11-10 lcp 1994-11-10 HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This ensures that if one dies, all die. BUT NOT Pure/Makefile, where PolyML.use"POLY" makes the identifier "use" visible.
1994-09-07 lcp 1994-09-07 addition of ZF/ex/twos_compl.thy
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-15 lcp 1994-08-15 ZF/Makefile/FILES: added many missing .thy files
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-07-21 nipkow 1994-07-21 added IMP
1994-07-12 lcp 1994-07-12 new cardinal arithmetic developments
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
1994-04-24 clasohm 1994-04-24 renamed theory files
1994-04-22 clasohm 1994-04-22 renamed theory files
1993-11-09 lcp 1993-11-09 Target "test" now depends on examples files
1993-11-04 clasohm 1993-11-04 renamed co_inductive.ML to coinductive.ML
1993-11-04 clasohm 1993-11-04 renamed some files
1993-10-27 lcp 1993-10-27 no longer specifies "-h 15000". Instead $ISABELLECOMP should include any switch settings.
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.thy to ord.thy
1993-10-11 clasohm 1993-10-11 renamed ordinal.ML to ord.ML
1993-10-06 clasohm 1993-10-06 rename list-fn to listfn
1993-09-16 clasohm 1993-09-16 Initial revision