1.1 --- a/NEWS	Fri Jan 06 10:19:48 2012 +0100
     1.2 +++ b/NEWS	Fri Jan 06 10:19:49 2012 +0100
     1.3 @@ -60,6 +60,26 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Consolidated theorem names concerning fold combinators:
     1.8 +  INFI_set_fold ~> INF_set_fold
     1.9 +  SUPR_set_fold ~> SUP_set_fold
    1.10 +  INF_code ~> INF_set_foldr
    1.11 +  SUP_code ~> SUP_set_foldr
    1.12 +  foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)
    1.13 +  foldl.simps ~> foldl_Nil foldl_Cons
    1.14 +  foldr_fold_rev ~> foldr_def
    1.15 +  foldl_fold ~> foldl_def
    1.16 +INCOMPATIBILITY.
    1.17 +
    1.18 +* Dropped rarely useful theorems concerning fold combinators: foldl_apply,
    1.19 +foldl_fun_comm, foldl_rev, fold_weak_invariant, rev_foldl_cons, fold_set_remdups,
    1.20 +fold_set, fold_set1, concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
    1.21 +foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, listsum_conv_fold,
    1.22 +listsum_foldl, sort_foldl_insort.  INCOMPATIBILITY.  Prefer "List.fold" with
    1.23 +canonical argument order, or boil down "List.foldr" and "List.foldl" to "List.fold"
    1.24 +by unfolding "foldr_def" and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
    1.25 +and "List.foldl plus 0", prefer "List.listsum".
    1.26 +
    1.27  * Concrete syntax for case expressions includes constraints for source
    1.28  positions, and thus produces Prover IDE markup for its bindings.
    1.29  INCOMPATIBILITY for old-style syntax translations that augment the
    1.30 @@ -82,7 +102,7 @@
    1.31  
    1.32  * 'set' is now a proper type constructor.  Definitions mem_def and Collect_def
    1.33  have disappeared.  INCOMPATIBILITY, rephrase sets S used as predicates by
    1.34 -`%x. x : S` and predicates P used as sets by `{x. P x}`.  For typical proofs,
    1.35 +"%x. x : S" and predicates P used as sets by "{x. P x}".  For typical proofs,
    1.36  it is often sufficent to prune any tinkering with former theorems mem_def
    1.37  and Collect_def.
    1.38