Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning whitespace in output syntax
authorblanchet
Sun, 14 Aug 2016 12:26:09 +0200
changeset 63689 61171cbeedde
parent 63688 cc57255bf6ae
child 63690 48a2c88091d7
tuning whitespace in output syntax
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle