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