NEWS

 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
 
 * 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>)'
   you can simply write `<simpset> addsplits <thms>'
 

   split_list_case and split_option_case.
 
 * 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;
 
 * added extended adm_tac to simplifier in HOLCF -- can now discharge
 adm (%x. P (t x)), where P is chainfinite and t continuous;