diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CCL/Set.thy
--- a/src/CCL/Set.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Set.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -18,7 +18,7 @@
   and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
 
 syntax
-  "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(1{_./ _})\<close>)
+  "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
 syntax_consts
   "_Coll" == Collect
 translations
@@ -50,8 +50,8 @@
   where "Bex(A, P) == EX x. x:A \<and> P(x)"
 
 syntax
-  "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(ALL _:_./ _)\<close> [0, 0, 0] 10)
-  "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(EX _:_./ _)\<close> [0, 0, 0] 10)
+  "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(\<open>notation=\<open>binder ALL:\<close>\<close>ALL _:_./ _)\<close> [0, 0, 0] 10)
+  "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(\<open>notation=\<open>binder EX:\<close>\<close>EX _:_./ _)\<close> [0, 0, 0] 10)
 syntax_consts
   "_Ball" == Ball and
   "_Bex" == Bex
@@ -127,8 +127,8 @@
   where "UNION(A, B) == {y. EX x:A. y: B(x)}"
 
 syntax
-  "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(INT _:_./ _)\<close> [0, 0, 0] 10)
-  "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(UN _:_./ _)\<close> [0, 0, 0] 10)
+  "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(\<open>notation=\<open>binder INT:\<close>\<close>INT _:_./ _)\<close> [0, 0, 0] 10)
+  "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(\<open>notation=\<open>binder UN:\<close>\<close>UN _:_./ _)\<close> [0, 0, 0] 10)
 syntax_consts
   "_INTER" == INTER and
   "_UNION" == UNION