# HG changeset patch
# User nipkow
# Date 1537703137 -7200
# Node ID 8d8fdbc02912680bf4fd66d378911c2a46de2636
# Parent  3ab140184a145292cb4e0d23698e62181e74e488
News

diff -r 3ab140184a14 -r 8d8fdbc02912 NEWS
--- 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 ***