--- a/src/HOL/Library/Multiset.thy Thu Nov 29 23:01:18 2007 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Nov 30 11:51:22 2007 +0100
@@ -25,8 +25,8 @@
"{#} = Abs_multiset (\<lambda>a. 0)"
definition
- single :: "'a => 'a multiset" ("{#_#}") where
- "{#a#} = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
+ single :: "'a => 'a multiset" where
+ "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
definition
count :: "'a multiset => 'a => nat" where
@@ -59,6 +59,13 @@
multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
"multiset_inter A B = A - (A - B)"
+syntax -- "Multiset Enumeration"
+ "@multiset" :: "args => 'a multiset" ("{#(_)#}")
+
+translations
+ "{#x, xs#}" == "{#x#} + {#xs#}"
+ "{#x#}" == "CONST single x"
+
text {*
\medskip Preservation of the representing set @{term multiset}.