diff -r be8c0e039a5e -r bc936d3d8b45 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CCL/Set.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -19,10 +19,10 @@
 
 syntax
   "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  ("(1{_./ _})")
+syntax_consts
+  "_Coll" == Collect
 translations
   "{x. P}" == "CONST Collect(\<lambda>x. P)"
-syntax_consts
-  "_Coll" == Collect
 
 lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
   apply (rule mem_Collect_iff [THEN iffD2])
@@ -52,12 +52,12 @@
 syntax
   "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(ALL _:_./ _)" [0, 0, 0] 10)
   "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(EX _:_./ _)" [0, 0, 0] 10)
+syntax_consts
+  "_Ball" == Ball and
+  "_Bex" == Bex
 translations
   "ALL x:A. P"  == "CONST Ball(A, \<lambda>x. P)"
   "EX x:A. P"   == "CONST Bex(A, \<lambda>x. P)"
-syntax_consts
-  "_Ball" == Ball and
-  "_Bex" == Bex
 
 lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
   by (simp add: Ball_def)
@@ -129,12 +129,12 @@
 syntax
   "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(INT _:_./ _)" [0, 0, 0] 10)
   "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(UN _:_./ _)" [0, 0, 0] 10)
+syntax_consts
+  "_INTER" == INTER and
+  "_UNION" == UNION
 translations
   "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
   "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
-syntax_consts
-  "_INTER" == INTER and
-  "_UNION" == UNION
 
 definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
   where "Inter(S) == (INT x:S. x)"