# HG changeset patch
# User oheimb
# Date 878652983 -3600
# Node ID 9600dd68d35b2e55079a7ed2eb80e6d26b1987d4
# Parent  f63c283cefafdf2e5289314b8e761a5a0b6e8ddf
*** empty log message ***

diff -r f63c283cefaf -r 9600dd68d35b NEWS
--- 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;