changeset 4154 | 17a3a2c5a35f |
parent 4125 | dc1cf9db1e17 |
child 4174 | 0a3556e5d6ed |
--- 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 ***