# HG changeset patch
# User haftmann
# Date 1324739699 -3600
# Node ID f6f582a5c5fd01bc1b478bcc020e6ec5afd77428
# Parent  989b1eede03cde077f49b5ff2650ee8e752bdffc
NEWS: `set` is now a proper type constructor

diff -r 989b1eede03c -r f6f582a5c5fd NEWS
--- 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.