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