# HG changeset patch
# User haftmann
# Date 1615101864 -3600
# Node ID 2e6b2134956e43aedf0b6881735ea1df726caed2
# Parent  716d256259d5c99ee73f0ac570bafc0be559cbf5
follow corresponding precedence on sets

diff -r 716d256259d5 -r 2e6b2134956e NEWS
--- a/NEWS	Sat Mar 06 18:42:10 2021 +0000
+++ b/NEWS	Sun Mar 07 08:24:24 2021 +0100
@@ -34,6 +34,10 @@
     multiset_inter_count ~> count_inter_mset
     sup_subset_mset_count ~> count_union_mset
 
+* Theory Multiset: syntax precendence for membership operations has been
+adjusted to match the corresponding precendences on sets.  Rare
+INCOMPATIBILITY.
+
 * HOL-Analysis/HOL-Probability: indexed products of discrete
 distributions, negative binomial distribution, Hoeffding's inequality,
 Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
diff -r 716d256259d5 -r 2e6b2134956e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Mar 06 18:42:10 2021 +0000
+++ b/src/HOL/Library/Multiset.thy	Sun Mar 07 08:24:24 2021 +0100
@@ -132,22 +132,22 @@
 
 notation
   member_mset  (\<open>'(\<in>#')\<close>) and
-  member_mset  (\<open>(_/ \<in># _)\<close> [51, 51] 50)
+  member_mset  (\<open>(_/ \<in># _)\<close> [50, 51] 50)
 
 notation  (ASCII)
   member_mset  (\<open>'(:#')\<close>) and
-  member_mset  (\<open>(_/ :# _)\<close> [51, 51] 50)
+  member_mset  (\<open>(_/ :# _)\<close> [50, 51] 50)
 
 abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
   where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>
 
 notation
   not_member_mset  (\<open>'(\<notin>#')\<close>) and
-  not_member_mset  (\<open>(_/ \<notin># _)\<close> [51, 51] 50)
+  not_member_mset  (\<open>(_/ \<notin># _)\<close> [50, 51] 50)
 
 notation  (ASCII)
   not_member_mset  (\<open>'(~:#')\<close>) and
-  not_member_mset  (\<open>(_/ ~:# _)\<close> [51, 51] 50)
+  not_member_mset  (\<open>(_/ ~:# _)\<close> [50, 51] 50)
 
 context
 begin