| changeset 35112 | ff6f60e6ab85 |
| parent 32960 | 69916a850301 |
| child 45602 | 2a858377c3d2 |
--- a/src/ZF/Induct/Multiset.thy Thu Feb 11 22:03:37 2010 +0100 +++ b/src/ZF/Induct/Multiset.thy Thu Feb 11 22:06:37 2010 +0100 @@ -74,9 +74,9 @@ "a :# M == a \<in> mset_of(M)" syntax - "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})") + "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})") syntax (xsymbols) - "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})") + "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})") translations "{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"