NEWS

 Use commands of the generic code generator instead.  INCOMPATIBILITY.
 
 * Redundant attribute 'code_inline' has been discontinued. Use
 'code_unfold' instead.  INCOMPATIBILITY.
 
-* Dropped attribute 'code_unfold_post' in favor of the its dual 'code_abbrev',
-which yields a common pattern in definitions like
+* Dropped attribute 'code_unfold_post' in favor of the its dual
+'code_abbrev', which yields a common pattern in definitions like
 
   definition [code_abbrev]: "f = t"
 
 INCOMPATIBILITY.
 

     -- "now uniform 'a::bar instead of default sort for first occurence (!)"
 
 
 *** HOL ***
 
-* Consolidated various theorem names relating to Finite_Set.fold combinator:
+* Type 'a set is now a proper type constructor (just as before
+Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
+Non-trivial 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
+Isabelle2011-1 before jumping right into the current release.
+
+* Consolidated various theorem names relating to Finite_Set.fold
+combinator:
+
   inf_INFI_fold_inf ~> inf_INF_fold_inf
   sup_SUPR_fold_sup ~> sup_SUP_fold_sup
   INFI_fold_inf ~> INF_fold_inf
   SUPR_fold_sup ~> SUP_fold_sup
   union_set ~> union_set_fold
   minus_set ~> minus_set_fold
   
 INCOMPATIBILITY.
 
 * Consolidated theorem names concerning fold combinators:
+
   INFI_set_fold ~> INF_set_fold
   SUPR_set_fold ~> SUP_set_fold
   INF_code ~> INF_set_foldr
   SUP_code ~> SUP_set_foldr
   foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)
   foldl.simps ~> foldl_Nil foldl_Cons
   foldr_fold_rev ~> foldr_def
   foldl_fold ~> foldl_def
+
 INCOMPATIBILITY.
 
-* Dropped rarely useful theorems concerning fold combinators: foldl_apply,
-foldl_fun_comm, foldl_rev, fold_weak_invariant, rev_foldl_cons, fold_set_remdups,
-fold_set, fold_set1, concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
-foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, listsum_conv_fold,
-listsum_foldl, sort_foldl_insort.  INCOMPATIBILITY.  Prefer "List.fold" with
-canonical argument order, or boil down "List.foldr" and "List.foldl" to "List.fold"
-by unfolding "foldr_def" and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
+* Dropped rarely useful theorems concerning fold combinators:
+foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
+rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
+concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
+foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
+listsum_conv_fold, listsum_foldl, sort_foldl_insort.  INCOMPATIBILITY.
+Prefer "List.fold" with canonical argument order, or boil down
+"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def"
+and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
 and "List.foldl plus 0", prefer "List.listsum".
 
 * Concrete syntax for case expressions includes constraints for source
 positions, and thus produces Prover IDE markup for its bindings.
 INCOMPATIBILITY for old-style syntax translations that augment the

 * Discontinued configuration option "syntax_positions": atomic terms
 in parse trees are always annotated by position constraints.
 
 * Finite_Set.fold now qualified.  INCOMPATIBILITY.
 
-* Renamed some facts on canonical fold on lists, in order to avoid problems
-with interpretation involving corresponding facts on foldl with the same base names:
+* Renamed some facts on canonical fold on lists, in order to avoid
+problems with interpretation involving corresponding facts on foldl
+with the same base names:
 
   fold_set_remdups ~> fold_set_fold_remdups
   fold_set ~> fold_set_fold
   fold1_set ~> fold1_set_fold
 
 INCOMPATIBILITY.
 
-* 'set' is now a proper type constructor.  Definitions mem_def and Collect_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.
+* Theory HOL/Library/AList has been renamed to
+  AList_Impl. INCOMPATIBILITY.
 
 * 'datatype' specifications allow explicit sort constraints.
 
-* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use
-theory HOL/Library/Nat_Bijection instead.
-
-* Session HOL-Word: Discontinued many redundant theorems specific to type
-'a word. INCOMPATIBILITY, use the corresponding generic theorems instead.
+* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
+use theory HOL/Library/Nat_Bijection instead.
+
+* Session HOL-Word: Discontinued many redundant theorems specific to
+type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
+instead.
 
   word_sub_alt ~> word_sub_wi
   word_add_alt ~> word_add_def
   word_mult_alt ~> word_mult_def
   word_minus_alt ~> word_minus_def