src/HOL/Makefile
1997-04-18 paulson 1997-04-18 ex/LFilter is a new theory (and dependency)
1997-04-09 paulson 1997-04-09 Dependency on Provers/nat_transitive
1997-04-04 paulson 1997-04-04 Added blast.ML as a dependency
1997-01-21 nipkow 1997-01-21 Modified MiniML. Added W0.
1996-12-19 paulson 1996-12-19 Addition of Auth/Recur
1996-12-10 paulson 1996-12-10 Now target "test" builds and tests TFL
1996-12-06 paulson 1996-12-06 Added public-key examples for Auth
1996-11-29 nipkow 1996-11-29 Modified dependencies for ex and Integ. (Rings)
1996-11-28 paulson 1996-11-28 Addition of Woo-Lam protocol
1996-11-27 paulson 1996-11-27 Makefile improvements by Thomas Santen and Stephan Herrmann Should be more portable across different versions of make
1996-10-21 paulson 1996-10-21 ISABELLECOMP may now have a leading pathname
1996-10-15 paulson 1996-10-15 Removed extraneous spaces from all Makefiles
1996-10-11 paulson 1996-10-11 Addition of OtwayRees_AN
1996-09-25 paulson 1996-09-25 Calls discgarb -c to realize dramatic space savings!
1996-09-24 nipkow 1996-09-24 Moved Option out of IOA into core HOL
1996-09-12 paulson 1996-09-12 New file cladata.ML
1996-09-10 paulson 1996-09-10 Added Auth to the test target
1996-07-15 paulson 1996-07-15 New dummy .thy files to document dependencies
1996-06-14 paulson 1996-06-14 Updated list of theories for target ex
1996-04-27 nipkow 1996-04-27 Forgot to add Expr to IMP.
1996-04-27 nipkow 1996-04-27 Updated IMP
1996-04-19 clasohm 1996-04-19 added thy_data.ML
1996-04-04 paulson 1996-04-04 New example Comb: Church-Rosser for combinators, ported from ZF
1996-03-27 paulson 1996-03-27 Added Mutil to ex targets
1996-02-19 nipkow 1996-02-19 Added dependency on RelPow
1996-02-10 clasohm 1996-02-10 make_html now only remains set if MAKE_HTML=true
1996-02-02 clasohm 1996-02-02 renamed subtype.ML to typedef.ML
1995-11-24 clasohm 1995-11-24 fixed make_html bug
1995-11-21 clasohm 1995-11-21 replaced exit_use by exit_use_dir
1995-11-21 clasohm 1995-11-21 replaced exit_use by exit_use_dir for subdirectories
1995-11-17 nipkow 1995-11-17 Added Lex
1995-11-17 nipkow 1995-11-17 Added Hoare.
1995-11-13 nipkow 1995-11-13 Put IOA back into test
1995-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-10-06 nipkow 1995-10-06 Added dependency on Eta
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-09-11 clasohm 1995-09-11 replaced "IOA/ROOT.ML" by "IOA/ROOT_NTP.ML IOA/ROOT_ABP.ML"
1995-09-11 clasohm 1995-09-11 split IOA/ROOT.ML into two files for ABP and NTP
1995-06-30 lcp 1995-06-30 added mention of new theories BT and Perm
1995-06-29 clasohm 1995-06-29 renamed CHOL to HOL
1995-05-27 nipkow 1995-05-27 Moved Relation from Integ to main HOL.
1995-05-22 nipkow 1995-05-22 Added Park induction to Lfp. Added Lambda to Makefile.
1995-04-16 nipkow 1995-04-16 Brought in line with new organization of IOA.
1995-04-13 lcp 1995-04-13 Simplified using pattern replacements.
1995-03-15 lcp 1995-03-15 Now calls exit_use instead of use, for prompt failure if errors are detected.
1995-03-08 nipkow 1995-03-08 Added dependencies on ../Provers/hypsubst.ML and removed those on ../Provers/ind.ML
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application