# HG changeset patch
# User nipkow
# Date 1227114931 -3600
# Node ID 5d21a3e7303cde2fc5272021e37eae22faa913aa
# Parent  c2b8be5ddc4a809d9d9c9ddf603bb97f09805a3a
*** empty log message ***

diff -r c2b8be5ddc4a -r 5d21a3e7303c NEWS
--- a/NEWS	Wed Nov 19 17:55:18 2008 +0100
+++ b/NEWS	Wed Nov 19 18:15:31 2008 +0100
@@ -169,6 +169,11 @@
 etc. slightly changed.  Some theorems named order_class.* now named
 preorder_class.*.
 
+* HOL/Finite_Set: added a new fold combinator of type
+  ('a => 'b => 'b) => 'b => 'a set => 'b
+Occasionally this is more convenient than the old fold combinator which is
+now defined in terms of the new one and renamed to fold_image.
+
 * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been
 moved to separate class dvd in Ring_and_Field; a couple of lemmas on
 dvd has been generalized to class comm_semiring_1.  Likewise a bunch