diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Set.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -21,34 +21,34 @@
 
 notation
   member  (\<open>'(\<in>')\<close>) and
-  member  (\<open>(_/ \<in> _)\<close> [51, 51] 50)
+  member  (\<open>(\<open>notation=\<open>infix \<in>\<close>\<close>_/ \<in> _)\<close> [51, 51] 50)
 
 abbreviation not_member
   where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> \<open>non-membership\<close>
 notation
   not_member  (\<open>'(\<notin>')\<close>) and
-  not_member  (\<open>(_/ \<notin> _)\<close> [51, 51] 50)
+  not_member  (\<open>(\<open>notation=\<open>infix \<notin>\<close>\<close>_/ \<notin> _)\<close> [51, 51] 50)
 
 notation (ASCII)
   member  (\<open>'(:')\<close>) and
-  member  (\<open>(_/ : _)\<close> [51, 51] 50) and
+  member  (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
   not_member  (\<open>'(~:')\<close>) and
-  not_member  (\<open>(_/ ~: _)\<close> [51, 51] 50)
+  not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
 
 
 text \<open>Set comprehensions\<close>
 
 syntax
-  "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    (\<open>(1{_./ _})\<close>)
+  "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
 syntax_consts
   "_Coll" \<rightleftharpoons> Collect
 translations
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
 syntax (ASCII)
-  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(1{(_/: _)./ _})\<close>)
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/: _)./ _})\<close>)
 syntax
-  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(1{(_/ \<in> _)./ _})\<close>)
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/ \<in> _)./ _})\<close>)
 syntax_consts
   "_Collect" \<rightleftharpoons> Collect
 translations
@@ -165,9 +165,9 @@
 
 notation
   subset  (\<open>'(\<subset>')\<close>) and
-  subset  (\<open>(_/ \<subset> _)\<close> [51, 51] 50) and
+  subset  (\<open>(\<open>notation=\<open>infix \<subset>\<close>\<close>_/ \<subset> _)\<close> [51, 51] 50) and
   subset_eq  (\<open>'(\<subseteq>')\<close>) and
-  subset_eq  (\<open>(_/ \<subseteq> _)\<close> [51, 51] 50)
+  subset_eq  (\<open>(\<open>notation=\<open>infix \<subseteq>\<close>\<close>_/ \<subseteq> _)\<close> [51, 51] 50)
 
 abbreviation (input)
   supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -179,15 +179,15 @@
 
 notation
   supset  (\<open>'(\<supset>')\<close>) and
-  supset  (\<open>(_/ \<supset> _)\<close> [51, 51] 50) and
+  supset  (\<open>(\<open>notation=\<open>infix \<supset>\<close>\<close>_/ \<supset> _)\<close> [51, 51] 50) and
   supset_eq  (\<open>'(\<supseteq>')\<close>) and
-  supset_eq  (\<open>(_/ \<supseteq> _)\<close> [51, 51] 50)
+  supset_eq  (\<open>(\<open>notation=\<open>infix \<supseteq>\<close>\<close>_/ \<supseteq> _)\<close> [51, 51] 50)
 
 notation (ASCII output)
   subset  (\<open>'(<')\<close>) and
-  subset  (\<open>(_/ < _)\<close> [51, 51] 50) and
+  subset  (\<open>(\<open>notation=\<open>infix <\<close>\<close>_/ < _)\<close> [51, 51] 50) and
   subset_eq  (\<open>'(<=')\<close>) and
-  subset_eq  (\<open>(_/ <= _)\<close> [51, 51] 50)
+  subset_eq  (\<open>(\<open>notation=\<open>infix <=\<close>\<close>_/ <= _)\<close> [51, 51] 50)
 
 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   \<comment> \<open>bounded universal quantifiers\<close>
@@ -196,21 +196,21 @@
   where "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> \<open>bounded existential quantifiers\<close>
 
 syntax (ASCII)
-  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3ALL (_/:_)./ _)\<close> [0, 0, 10] 10)
-  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3EX (_/:_)./ _)\<close> [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3EX! (_/:_)./ _)\<close> [0, 0, 10] 10)
-  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           (\<open>(3LEAST (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder ALL :\<close>\<close>ALL (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder EX :\<close>\<close>EX (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder EX! :\<close>\<close>EX! (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           (\<open>(\<open>indent=3 notation=\<open>binder LEAST :\<close>\<close>LEAST (_/:_)./ _)\<close> [0, 0, 10] 10)
 
 syntax (input)
-  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3! (_/:_)./ _)\<close> [0, 0, 10] 10)
-  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3? (_/:_)./ _)\<close> [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3?! (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder ! :\<close>\<close>! (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder ? :\<close>\<close>? (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder ?! :\<close>\<close>?! (_/:_)./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<forall>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
-  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>!(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
-  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           (\<open>(3LEAST(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(\<open>indent=3 notation=\<open>binder \<exists>!\<close>\<close>\<exists>!(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           (\<open>(\<open>indent=3 notation=\<open>binder LEAST\<close>\<close>LEAST(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_Ball" \<rightleftharpoons> Ball and
@@ -225,18 +225,18 @@
   "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
 
 syntax (ASCII output)
-  "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(3ALL _<_./ _)\<close>  [0, 0, 10] 10)
-  "_setlessEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(3EX _<_./ _)\<close>  [0, 0, 10] 10)
-  "_setleAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(3ALL _<=_./ _)\<close> [0, 0, 10] 10)
-  "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(3EX _<=_./ _)\<close> [0, 0, 10] 10)
-  "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(3EX! _<=_./ _)\<close> [0, 0, 10] 10)
+  "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<_./ _)\<close>  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<_./ _)\<close>  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<=_./ _)\<close> [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<=_./ _)\<close> [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder EX!\<close>\<close>EX! _<=_./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<forall>_\<subset>_./ _)\<close>  [0, 0, 10] 10)
-  "_setlessEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<exists>_\<subset>_./ _)\<close>  [0, 0, 10] 10)
-  "_setleAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<forall>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
-  "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<exists>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
-  "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<exists>!_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+  "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<subset>_./ _)\<close>  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<subset>_./ _)\<close>  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder \<exists>!\<close>\<close>\<exists>!_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_setlessAll" "_setleAll" \<rightleftharpoons> All and
@@ -291,7 +291,8 @@
 \<close>
 
 syntax
-  "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set"    (\<open>(1{_ |/_./ _})\<close>)
+  "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ |/_./ _})\<close>)
 syntax_consts
   "_Setcompr" \<rightleftharpoons> Collect