tuned syntax declaration;
authorwenzelm
Thu, 28 Feb 2008 12:56:31 +0100
changeset 26176 038baad81209
parent 26175 11e338832c31
child 26177 6b127c056e83
tuned syntax declaration;
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"