author | nipkow |
Sun, 23 Sep 2018 13:45:37 +0200 | |
changeset 69037 | 8d8fdbc02912 |
parent 69036 | 3ab140184a14 |
child 69038 | 2ce9bc515a64 |
--- a/NEWS Sun Sep 23 12:50:12 2018 +0200 +++ b/NEWS Sun Sep 23 13:45:37 2018 +0200 @@ -35,6 +35,9 @@ and prod_mset.swap, similarly to sum.swap and prod.swap. INCOMPATIBILITY. +* Theory "HOL-Library.Multiset": the <Union># operator now has the same +precedence as any other prefix function symbol. + *** ML ***