1.1 --- a/NEWS	Fri Jan 06 17:44:42 2012 +0100
     1.2 +++ b/NEWS	Fri Jan 06 10:53:52 2012 +0100
     1.3 @@ -101,10 +101,15 @@
     1.4  INCOMPATIBILITY.
     1.5  
     1.6  * 'set' is now a proper type constructor.  Definitions mem_def and Collect_def
     1.7 -have disappeared.  INCOMPATIBILITY, rephrase sets S used as predicates by
     1.8 -"%x. x : S" and predicates P used as sets by "{x. P x}".  For typical proofs,
     1.9 -it is often sufficent to prune any tinkering with former theorems mem_def
    1.10 +have disappeared.  INCOMPATIBILITY.
    1.11 +For developments keeping predicates and sets
    1.12 +separate, it is often sufficient to rephrase sets S accidentally used as predicates by
    1.13 +"%x. x : S" and predicates P accidentally used as sets by "{x. P x}".  Corresponding
    1.14 +proofs in a first step should be pruned from any tinkering with former theorems mem_def
    1.15  and Collect_def.
    1.16 +For developments which deliberately mixed predicates and sets, a planning step is
    1.17 +necessary to determine what should become a predicate and what a set.  It can be helpful
    1.18 +to carry out that step in Isabelle 2011-1 before jumping to the current release.
    1.19  
    1.20  * Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY.
    1.21