--- 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