equal
deleted
inserted
replaced
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 "HOLLibrary.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 