--- a/NEWS Tue Nov 04 14:40:29 1997 +0100
+++ b/NEWS Tue Nov 04 15:16:23 1997 +0100
@@ -122,10 +122,22 @@
* HOL/Lists: the function "set_of_list" has been renamed "set"
(and its theorems too);
-
*** HOLCF ***
-* HOLCF: fixed LAM <x,y,zs>.b syntax;
+* 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: proves theorems immediately and stores them in the theory
+ creates hierachical name space
+ now uses normal mixfix annotations (instead of cinfix...)
+ 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 defs: changed "," to "and"
+ improved handling of sort constraints. Now they have to
+ appear on the left-hand side of the equations only.
+
+* fixed LAM <x,y,zs>.b syntax;
* added extended adm_tac to simplifier in HOLCF -- can now discharge
adm (%x. P (t x)), where P is chainfinite and t continuous;