NEWS: `set` is now a proper type constructor

--- a/NEWS	Sat Dec 24 16:14:58 2011 +0100
+++ b/NEWS	Sat Dec 24 16:14:59 2011 +0100
@@ -53,6 +53,12 @@
 
 *** HOL ***
 
+* 'set' is now a proper type constructor.  Definitions mem_def and Collect_def
+have disappeared.  INCOMPATIBILITY, rephrase sets S used as predicates by
+`%x. x : S` and predicates P used as sets by `{x. P x}`.  For typical proofs,
+it is often sufficent to prune any tinkering with former theorems mem_def
+and Collect_def.
+
 * Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPABILITY.
 
 * 'datatype' specifications allow explicit sort constraints.