equal
deleted
inserted
replaced
51 * Theory List: the precedence of the list_update operator has changed: |
51 * Theory List: the precedence of the list_update operator has changed: |
52 "f a [n := x]" now needs to be written "(f a)[n := x]". |
52 "f a [n := x]" now needs to be written "(f a)[n := x]". |
53 |
53 |
54 * Theory "HOL-Library.Multiset": the <Union># operator now has the same |
54 * Theory "HOL-Library.Multiset": the <Union># operator now has the same |
55 precedence as any other prefix function symbol. |
55 precedence as any other prefix function symbol. |
|
56 |
|
57 * Retired lemma card_Union_image; use the simpler card_UN_disjoint instead. |
56 |
58 |
57 * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap |
59 * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap |
58 and prod_mset.swap, similarly to sum.swap and prod.swap. |
60 and prod_mset.swap, similarly to sum.swap and prod.swap. |
59 INCOMPATIBILITY. |
61 INCOMPATIBILITY. |
60 |
62 |