# HG changeset patch
# User haftmann
# Date 1331152709 -3600
# Node ID a5fa1dc5594534d547d57494571c963fcb4a4692
# Parent  85619a872ab541379dfa24c07244df9e8c9a9f61
less rigorous but more realistic migration recommendation; note on code generation of sets

diff -r 85619a872ab5 -r a5fa1dc55945 NEWS
--- a/NEWS	Wed Mar 07 21:34:36 2012 +0100
+++ b/NEWS	Wed Mar 07 21:38:29 2012 +0100
@@ -83,11 +83,15 @@
 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
+Collect_def as far as possible.
+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
 Isabelle2011-1 before jumping right into the current release.
 
+* Code generation by default implements sets as container type rather
+than predicates.  INCOMPATIBILITY.
+
 * New type synonym 'a rel = ('a * 'a) set
 
 * More default pred/set conversions on a couple of relation operations