diff -r 1af16493c57f -r dc1cf9db1e17 NEWS
--- 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;