| changeset 80754 | 701912f5645a |
| parent 76217 | 8655344f1cf6 |
| child 80761 | bc936d3d8b45 |
--- a/src/ZF/Induct/Multiset.thy Fri Aug 23 22:47:51 2024 +0200 +++ b/src/ZF/Induct/Multiset.thy Fri Aug 23 23:14:39 2024 +0200 @@ -77,6 +77,7 @@ "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>) translations "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)" +syntax_consts "_MColl" \<rightleftharpoons> MCollect (* multiset orderings *)