NEWS
changeset 49822 0cfc1651be25
parent 49770 cf6a78acf445
child 49836 c13b39542972
--- a/NEWS	Thu Oct 11 00:13:21 2012 +0200
+++ b/NEWS	Thu Oct 11 11:56:42 2012 +0200
@@ -62,6 +62,16 @@
 
 *** HOL ***
 
+* Theory "Library/Multiset":
+
+  - Renamed constants
+      fold_mset ~> Multiset.fold  -- for coherence with other fold combinators
+
+  - Renamed facts
+      fold_mset_commute ~> fold_mset_comm  -- for coherence with fold_comm
+
+INCOMPATIBILITY.
+
 * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
 
 * Class "comm_monoid_diff" formalises properties of bounded