NEWS
changeset 69037 8d8fdbc02912
parent 68938 a0b19a163f5e
child 69042 6e9df530b441
equal deleted inserted replaced
69036:3ab140184a14 69037:8d8fdbc02912
    32 provers, has been updated.
    32 provers, has been updated.
    33 
    33 
    34 * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
    34 * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
    35 and prod_mset.swap, similarly to sum.swap and prod.swap.
    35 and prod_mset.swap, similarly to sum.swap and prod.swap.
    36 INCOMPATIBILITY.
    36 INCOMPATIBILITY.
       
    37 
       
    38 * Theory "HOL-Library.Multiset": the <Union># operator now has the same
       
    39 precedence as any other prefix function symbol.
    37 
    40 
    38 
    41 
    39 *** ML ***
    42 *** ML ***
    40 
    43 
    41 * Original PolyML.pointerEq is retained as a convenience for tools that
    44 * Original PolyML.pointerEq is retained as a convenience for tools that