diff -r e534c4c32d54 -r 17a3a2c5a35f NEWS --- 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 ***