1998-09-21 oheimb 1998-09-21 added dependance on HOL
1997-11-04 wenzelm 1997-11-04 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
1997-11-04 wenzelm 1997-11-04 tuned to make non-Poly/MLs happy;
1997-11-04 oheimb 1997-11-04 * removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)
1997-10-30 oheimb 1997-10-30 domain package: * theorems are stored in the theory * creates hierachical name space * minor changes to some names and values (for consistency), e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas * separator between mutual domain definitions changed from "," to "and" * minor debugging of Domain_Library.mk_var_names
1997-10-27 wenzelm 1997-10-27 do not change global_names flag;
1997-10-27 oheimb 1997-10-27 adapted domain and ax_ops package for name spaces
1997-10-20 wenzelm 1997-10-20 set global_names;
1997-08-06 wenzelm 1997-08-06 tuned; removed qed_spec_mp;
1997-08-06 berghofe 1997-08-06 Replaced "init_thy_reader" by set_parser.
1997-07-09 wenzelm 1997-07-09 removed obsolete init_pps and init_thy_reader;
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-12-09 sandnerr 1996-12-09 qed_spec_mp moved to end of file
1996-11-29 wenzelm 1996-11-29 added qed_spec_mp (from HOL);
1996-11-29 oheimb 1996-11-29 *** empty log message ***
1996-11-29 oheimb 1996-11-29 renamed is_flat to flat, moved Lift*.* to Up*.*, renaming of all constans and theorems concerned, (*lift* to *up*, except Ilift to Ifup, lift to fup)
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-05-31 oheimb 1996-05-31 introduced forgotten bind_thm calls
1996-03-12 regensbu 1996-03-12 added ' make_html:=false;' to end of ROOT file
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-25 clasohm 1995-10-25 added init_html and make_chart
1995-10-17 regensbu 1995-10-17 removed incompatibility with sml
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-06-29 regensbu 1995-06-29 The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported
1995-03-17 regensbu 1995-03-17 Removed bugs which occurred due to new generation mechanism for type variables
1994-10-06 nipkow 1994-10-06 New version
1994-05-19 wenzelm 1994-05-19 thy reader now initialised by init_thy_reader();
1994-03-24 nipkow 1994-03-24 Franz fragen
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.