# HG changeset patch
# User nipkow
# Date 1201885266 -3600
# Node ID 278025d5282dd19eef9bbdd5e25c7d2fc83e9125
# Parent  377b7aa0b5b50ca6483f2593aec71f0e11c55873
modified MCollect syntax

diff -r 377b7aa0b5b5 -r 278025d5282d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 01 08:35:58 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 01 18:01:06 2008 +0100
@@ -46,9 +46,9 @@
 notation (xsymbols) Melem (infix "\<in>#" 50)
 
 syntax
-  "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
+  "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ :# _./ _#})")
 translations
-  "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)"
+  "{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
 
 definition
   set_of :: "'a multiset => 'a set" where
@@ -178,7 +178,7 @@
 by (simp add: count_def diff_def in_multiset)
 
 lemma count_MCollect [simp]:
-  "count {# x:M. P x #} a = (if P a then count M a else 0)"
+  "count {# x:#M. P x #} a = (if P a then count M a else 0)"
 by (simp add: count_def MCollect_def in_multiset)
 
 
@@ -199,7 +199,7 @@
 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
 by (auto simp add: set_of_def)
 
-lemma set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
+lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
 by (auto simp add: set_of_def)
 
 
@@ -473,7 +473,7 @@
   apply (rule_tac x="M - {#x#}" in exI, simp)
   done
 
-lemma multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
+lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
   by (subst multiset_eq_conv_count_eq, auto)
 
 declare multiset_typedef [simp del]
@@ -678,8 +678,8 @@
   apply (erule ssubst)
   apply (simp add: Ball_def, auto)
   apply (subgoal_tac
-    "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
-      (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
+    "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
+      (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
    prefer 2
    apply force
   apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
@@ -1334,9 +1334,9 @@
 syntax comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
        ("({#_/ | _ :# _./ _#})")
 translations
-  "{#e | x:#M. P#}" => "{#e. x :# {# x:M. P#}#}"
+  "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
 
-text{* This allows to write not just filters like @{term"{#x:M. x<c#}"}
+text{* This allows to write not just filters like @{term"{#x:#M. x<c#}"}
 but also images like @{term"{#x+x. x:#M #}"}
 and @{term[source]"{#x+x|x:#M. x<c#}"}, where the latter is currently
 displayed as @{term"{#x+x|x:#M. x<c#}"}. *}