src/ZF/Induct/Multiset.thy

--- a/src/ZF/Induct/Multiset.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -53,7 +53,7 @@
 
 definition
   (* set of elements of a multiset *)
-  msingle :: "i \<Rightarrow> i"    (\<open>{#_#}\<close>)  where
+  msingle :: "i \<Rightarrow> i"    (\<open>(\<open>open_block notation=\<open>mixfix multiset\<close>\<close>{#_#})\<close>)  where
   "{#a#} \<equiv> {\<langle>a, 1\<rangle>}"
 
 definition