--- a/src/ZF/Induct/Multiset.thy Sun Sep 29 21:57:47 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Sun Sep 29 22:47:14 2024 +0200
@@ -74,7 +74,7 @@
"a :# M \<equiv> a \<in> mset_of(M)"
syntax
- "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
+ "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{# _ \<in> _./ _#})\<close>)
syntax_consts
MCollect
translations