| changeset 20770 | 2c583720436e |
| parent 20503 | 503ac4c5ef91 |
| child 21214 | a91bab12b2bd |
--- a/src/HOL/Library/Multiset.thy Thu Sep 28 23:42:39 2006 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Sep 28 23:42:43 2006 +0200 @@ -40,7 +40,7 @@ syntax "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") translations - "{#x:M. P#}" == "MCollect M (\<lambda>x. P)" + "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)" definition set_of :: "'a multiset => 'a set"