NEWS
changeset 49822 0cfc1651be25
parent 49770 cf6a78acf445
child 49836 c13b39542972
     1.1 --- a/NEWS	Thu Oct 11 00:13:21 2012 +0200
     1.2 +++ b/NEWS	Thu Oct 11 11:56:42 2012 +0200
     1.3 @@ -62,6 +62,16 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory "Library/Multiset":
     1.8 +
     1.9 +  - Renamed constants
    1.10 +      fold_mset ~> Multiset.fold  -- for coherence with other fold combinators
    1.11 +
    1.12 +  - Renamed facts
    1.13 +      fold_mset_commute ~> fold_mset_comm  -- for coherence with fold_comm
    1.14 +
    1.15 +INCOMPATIBILITY.
    1.16 +
    1.17  * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
    1.18  
    1.19  * Class "comm_monoid_diff" formalises properties of bounded