--- a/NEWS Tue Nov 04 16:17:04 1997 +0100
+++ b/NEWS Tue Nov 04 16:21:52 1997 +0100
@@ -91,7 +91,7 @@
* HOL/Auth: new protocol proofs including some for the Internet
protocol TLS;
-* HOL/Map: new theory of `maps' a la VDM.
+* HOL/Map: new theory of `maps' a la VDM;
* HOL/simplifier: added infix function `addsplits':
instead of `<simpset> setloop (split_tac <thms>)'
@@ -122,20 +122,23 @@
* HOL/Lists: the function "set_of_list" has been renamed "set"
(and its theorems too);
+
*** HOLCF ***
-* removed "axioms" and "generated by" section
+* removed "axioms" and "generated by" sections;
+
* 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.
+ 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;