# HG changeset patch
# User nipkow
# Date 1196419882 -3600
# Node ID d13468d4013149de829a45b78e2e8fef0b34068b
# Parent  c9bea6426932af9cd07cb489dca9694e8a30e8be
added {#.,.,...#}

diff -r c9bea6426932 -r d13468d40131 src/HOL/Library/Multiset.thy
--- 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}.