# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID 61171cbeedde1eb71d4e3c122b013c4518a8241e
# Parent  cc57255bf6ae7d7bd08e8b8cf01d148c8235ab44
tuning whitespace in output syntax

diff -r cc57255bf6ae -r 61171cbeedde src/HOL/Library/Multiset.thy
--- 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"