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

Tobias

Reply via email to