# HG changeset patch
# User wenzelm
# Date 1326116838 -3600
# Node ID f363e5a2f8e810e599780f3032be99b4fce1c549
# Parent  05a82dd869ed2d6141632da2298c0a180806f447
misc tuning and reformatting;

diff -r 05a82dd869ed -r f363e5a2f8e8 NEWS
--- a/NEWS	Mon Jan 09 14:26:13 2012 +0100
+++ b/NEWS	Mon Jan 09 14:47:18 2012 +0100
@@ -41,8 +41,8 @@
 * 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"
 
@@ -60,7 +60,21 @@
 
 *** 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
@@ -71,6 +85,7 @@
 INCOMPATIBILITY.
 
 * Consolidated theorem names concerning fold combinators:
+
   INFI_set_fold ~> INF_set_fold
   SUPR_set_fold ~> SUP_set_fold
   INF_code ~> INF_set_foldr
@@ -79,15 +94,18 @@
   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
@@ -101,8 +119,9 @@
 
 * 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
@@ -110,26 +129,17 @@
 
 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