--- a/src/CCL/Set.thy Thu Oct 10 12:19:50 2024 +0200
+++ b/src/CCL/Set.thy Thu Oct 10 12:20:24 2024 +0200
@@ -100,7 +100,7 @@
definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"
where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
-definition singleton :: "'a \<Rightarrow> 'a set" (\<open>{_}\<close>)
+definition singleton :: "'a \<Rightarrow> 'a set" (\<open>(\<open>open_block notation=\<open>mixfix singleton\<close>\<close>{_})\<close>)
where "{a} == {x. x=a}"
definition empty :: "'a set" (\<open>{}\<close>)