--- a/src/ZF/Induct/Multiset.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Fri Sep 20 23:37:00 2024 +0200
@@ -70,11 +70,11 @@
"msize(M) \<equiv> setsum(\<lambda>a. $# mcount(M,a), mset_of(M))"
abbreviation
- melem :: "[i,i] \<Rightarrow> o" (\<open>(_/ :# _)\<close> [50, 51] 50) where
+ melem :: "[i,i] \<Rightarrow> o" (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<close> [50, 51] 50) where
"a :# M \<equiv> a \<in> mset_of(M)"
syntax
- "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
+ "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
syntax_consts "_MColl" \<rightleftharpoons> MCollect
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"