# HG changeset patch # User wenzelm # Date 1204199791 -3600 # Node ID 038baad81209c2183e8adeaf84bca65fb219c0dd # Parent 11e338832c31dd964fa1e4a24bc5896c5c3e1faa tuned syntax declaration; diff -r 11e338832c31 -r 038baad81209 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Feb 28 12:56:30 2008 +0100 +++ b/src/HOL/Library/Multiset.thy Thu Feb 28 12:56:31 2008 +0100 @@ -81,7 +81,7 @@ text {* Multiset Enumeration *} syntax - "@multiset" :: "args => 'a multiset" ("{#(_)#}") + "_multiset" :: "args => 'a multiset" ("{#(_)#}") translations "{#x, xs#}" == "{#x#} + {#xs#}" "{#x#}" == "CONST single x"