src/HOL/Library/Multiset.thy
changeset 35352 fa051b504c3f
parent 35308 359e0fd38a92
child 35402 115a5a95710a
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Feb 24 20:37:01 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Feb 24 21:55:46 2010 +0100
     1.3 @@ -1502,13 +1502,13 @@
     1.4  by (cases M) auto
     1.5  
     1.6  syntax
     1.7 -  comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
     1.8 +  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
     1.9        ("({#_/. _ :# _#})")
    1.10  translations
    1.11    "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
    1.12  
    1.13  syntax
    1.14 -  comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
    1.15 +  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
    1.16        ("({#_/ | _ :# _./ _#})")
    1.17  translations
    1.18    "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"