UNIV & UNION1

--- a/NEWS	Wed Nov 05 13:23:46 1997 +0100
+++ b/NEWS	Wed Nov 05 13:25:34 1997 +0100
@@ -122,6 +122,11 @@
 * HOL/Lists: the function "set_of_list" has been renamed "set"
   (and its theorems too);
 
+* HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
+
+* HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
+  specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
+
 
 *** HOLCF ***