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 "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 |