src/HOL/Makefile
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