# HG changeset patch
# User haftmann
# Date 1325843632 -3600
# Node ID ab21fc844ea260d2605f3bf8d419b7238c3ef4c5
# Parent  85f8d8a8c711bdf6043158e911dae09dc779626d
more explicit NEWS

diff -r 85f8d8a8c711 -r ab21fc844ea2 NEWS
--- a/NEWS	Fri Jan 06 17:44:42 2012 +0100
+++ b/NEWS	Fri Jan 06 10:53:52 2012 +0100
@@ -101,10 +101,15 @@
 INCOMPATIBILITY.
 
 * '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
+have disappeared.  INCOMPATIBILITY.
+For developments keeping predicates and sets
+separate, it is often sufficient to rephrase sets S accidentally used as predicates by
+"%x. x : S" and predicates P accidentally used as sets by "{x. P x}".  Corresponding
+proofs in a first step should be pruned from any tinkering with former theorems mem_def
 and Collect_def.
+For developments which deliberately mixed predicates and sets, a planning step is
+necessary to determine what should become a predicate and what a set.  It can be helpful
+to carry out that step in Isabelle 2011-1 before jumping to the current release.
 
 * Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY.