--- a/src/HOL/Library/Multiset.thy Sat Aug 13 23:45:29 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Sun Aug 14 12:26:09 2016 +0200
@@ -1027,9 +1027,9 @@
by (rule filter_preserves_multiset)
syntax (ASCII)
- "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})")
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{#_ :# _./ _#})")
syntax
- "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})")
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{#_ \<in># _./ _#})")
translations
"{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"