# HG changeset patch
# User wenzelm
# Date 1727118563 -7200
# Node ID 8e72f55295fd9caf41b0b698dc35ddf77e5e8419
# Parent  56f1c0af602c3ffc6acca1d5ca4801de046c9319
more inner syntax markup: HOL;

diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -273,7 +273,7 @@
 (* Similar setup to the one for SIGMA from theory Big_Operators: *)
 syntax "_Csum" ::
   "pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
-  (\<open>(3CSUM _:_. _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder CSUM\<close>\<close>CSUM _:_. _)\<close> [0, 51, 10] 10)
 
 syntax_consts
   "_Csum" == Csum
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Complete_Lattices.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -21,16 +21,16 @@
   fixes Sup :: "'a set \<Rightarrow> 'a"  (\<open>\<Squnion> _\<close> [900] 900)
 
 syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3INF _./ _)\<close> [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3INF _\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3SUP _./ _)\<close> [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3SUP _\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder INF\<close>\<close>INF _./ _)\<close> [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder INF\<close>\<close>INF _\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder SUP\<close>\<close>SUP _./ _)\<close> [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder SUP\<close>\<close>SUP _\<in>_./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_INF1" "_INF" \<rightleftharpoons> Inf and
@@ -843,12 +843,12 @@
 subsubsection \<open>Intersections of families\<close>
 
 syntax (ASCII)
-  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           (\<open>(3INT _./ _)\<close> [0, 10] 10)
-  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  (\<open>(3INT _:_./ _)\<close> [0, 0, 10] 10)
+  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _./ _)\<close> [0, 10] 10)
+  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _:_./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           (\<open>(3\<Inter>_./ _)\<close> [0, 10] 10)
-  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  (\<open>(3\<Inter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_./ _)\<close> [0, 10] 10)
+  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 syntax (latex output)
   "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           (\<open>(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
@@ -1009,12 +1009,12 @@
 subsubsection \<open>Unions of families\<close>
 
 syntax (ASCII)
-  "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(3UN _./ _)\<close> [0, 10] 10)
-  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (\<open>(3UN _:_./ _)\<close> [0, 0, 10] 10)
+  "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _./ _)\<close> [0, 10] 10)
+  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _:_./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(3\<Union>_./ _)\<close> [0, 10] 10)
-  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (\<open>(3\<Union>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_./ _)\<close> [0, 10] 10)
+  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 syntax (latex output)
   "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Deriv.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -70,7 +70,7 @@
 \<close>
 abbreviation (input)
   FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  (\<open>(FDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+  (\<open>(\<open>notation=\<open>mixfix FDERIV\<close>\<close>FDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
   where "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
 
 lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
@@ -782,7 +782,7 @@
 
 abbreviation (input)
   DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-    (\<open>(DERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+    (\<open>(\<open>notation=\<open>mixfix DERIV\<close>\<close>DERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
   where "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
 
 abbreviation has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool"
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Filter.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -40,7 +40,7 @@
   where "eventually P F \<longleftrightarrow> Rep_filter F P"
 
 syntax
-  "_eventually" :: "pttrn => 'a filter => bool => bool"  (\<open>(3\<forall>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
+  "_eventually" :: "pttrn => 'a filter => bool => bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<^sub>F\<close>\<close>\<forall>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_eventually" == eventually
 translations
@@ -160,7 +160,7 @@
   where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
 
 syntax
-  "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3\<exists>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
+  "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<^sub>F\<close>\<close>\<exists>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_frequently" == frequently
 translations
@@ -1307,7 +1307,7 @@
   "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
 
 syntax
-  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(3LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
+  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder LIM\<close>\<close>LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
 
 syntax_consts
   "_LIM" == filterlim
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Fun.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -841,10 +841,10 @@
 nonterminal updbinds and updbind
 
 syntax
-  "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             (\<open>(2_ :=/ _)\<close>)
+  "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   ""         :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
-  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((_)')\<close> [1000, 0] 900)
+  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((\<open>indent=2 notation=\<open>mixfix updates\<close>\<close>_)')\<close> [1000, 0] 900)
 
 syntax_consts
   "_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/GCD.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -148,10 +148,10 @@
     and Lcm :: "'a set \<Rightarrow> 'a"
 
 syntax
-  "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3GCD _./ _)\<close> [0, 10] 10)
-  "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3GCD _\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3LCM _./ _)\<close> [0, 10] 10)
-  "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3LCM _\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder GCD\<close>\<close>GCD _./ _)\<close> [0, 10] 10)
+  "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder GCD\<close>\<close>GCD _\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder LCM\<close>\<close>LCM _./ _)\<close> [0, 10] 10)
+  "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder LCM\<close>\<close>LCM _\<in>_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_GCD1" "_GCD" \<rightleftharpoons> Gcd and
@@ -2851,7 +2851,7 @@
 definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat" 
   where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
 
-syntax "_type_char" :: "type => nat" (\<open>(1CHAR/(1'(_')))\<close>)
+syntax "_type_char" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>prefix CHAR\<close>\<close>CHAR/(1'(_')))\<close>)
 syntax_consts "_type_char" \<rightleftharpoons> semiring_char
 translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
 print_translation \<open>
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -651,9 +651,9 @@
 text \<open>Now: lots of fancy syntax. First, \<^term>\<open>sum (\<lambda>x. e) A\<close> is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
 
 syntax (ASCII)
-  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  (\<open>(3SUM (_/:_)./ _)\<close> [0, 51, 10] 10)
+  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM (_/:_)./ _)\<close> [0, 51, 10] 10)
 syntax
-  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  (\<open>(2\<Sum>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
 
 syntax_consts
   "_sum" \<rightleftharpoons> sum
@@ -665,9 +665,9 @@
 text \<open>Instead of \<^term>\<open>\<Sum>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
 
 syntax (ASCII)
-  "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3SUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+  "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder SUM Collect\<close>\<close>SUM _ |/ _./ _)\<close> [0, 0, 10] 10)
 syntax
-  "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(2\<Sum>_ | (_)./ _)\<close> [0, 0, 10] 10)
+  "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum> Collect\<close>\<close>\<Sum>_ | (_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_qsum" == sum
@@ -1421,9 +1421,9 @@
 end
 
 syntax (ASCII)
-  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  (\<open>(4PROD (_/:_)./ _)\<close> [0, 51, 10] 10)
+  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  (\<open>(\<open>indent=4 notation=\<open>binder PROD\<close>\<close>PROD (_/:_)./ _)\<close> [0, 51, 10] 10)
 syntax
-  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  (\<open>(2\<Prod>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  (\<open>(\<open>indent=2 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
 
 syntax_consts
   "_prod" == prod
@@ -1435,9 +1435,9 @@
 text \<open>Instead of \<^term>\<open>\<Prod>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
 
 syntax (ASCII)
-  "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(4PROD _ |/ _./ _)\<close> [0, 0, 10] 10)
+  "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=4 notation=\<open>binder PROD Collect\<close>\<close>PROD _ |/ _./ _)\<close> [0, 0, 10] 10)
 syntax
-  "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(2\<Prod>_ | (_)./ _)\<close> [0, 0, 10] 10)
+  "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Prod> Collect\<close>\<close>\<Prod>_ | (_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_qprod" == prod
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Groups_List.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -98,9 +98,9 @@
 
 text \<open>Some syntactic sugar for summing a function over a list:\<close>
 syntax (ASCII)
-  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(3SUM _<-_. _)\<close> [0, 51, 10] 10)
+  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _<-_. _)\<close> [0, 51, 10] 10)
 syntax
-  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(3\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
+  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_sum_list" == sum_list
 translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -597,9 +597,9 @@
 text \<open>Some syntactic sugar:\<close>
 
 syntax (ASCII)
-  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(3PROD _<-_. _)\<close> [0, 51, 10] 10)
+  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _<-_. _)\<close> [0, 51, 10] 10)
 syntax
-  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(3\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
+  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_prod_list" \<rightleftharpoons> prod_list
 translations \<comment> \<open>Beware of argument permutation!\<close>
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -81,7 +81,7 @@
 
 typedecl bool
 
-judgment Trueprop :: "bool \<Rightarrow> prop"  (\<open>(_)\<close> 5)
+judgment Trueprop :: "bool \<Rightarrow> prop"  (\<open>(\<open>notation=judgment\<close>_)\<close> 5)
 
 axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr \<open>\<longrightarrow>\<close> 25)
   and eq :: "['a, 'a] \<Rightarrow> bool"
@@ -127,8 +127,8 @@
 
 subsubsection \<open>Additional concrete syntax\<close>
 
-syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(4?< _./ _)\<close> [0, 10] 10)
-syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
+syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=4 notation=\<open>binder ?<\<close>\<close>?< _./ _)\<close> [0, 10] 10)
+syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=2 notation=\<open>binder \<exists>\<^sub>\<le>\<^sub>1\<close>\<close>\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
 
 syntax_consts "_Uniq" \<rightleftharpoons> Uniq
 
@@ -140,10 +140,10 @@
 
 
 syntax (ASCII)
-  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3EX! _./ _)\<close> [0, 10] 10)
+  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder EX!\<close>\<close>EX! _./ _)\<close> [0, 10] 10)
 syntax (input)
-  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3?! _./ _)\<close> [0, 10] 10)
-syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3\<exists>!_./ _)\<close> [0, 10] 10)
+  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder ?!\<close>\<close>?! _./ _)\<close> [0, 10] 10)
+syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<exists>!\<close>\<close>\<exists>!_./ _)\<close> [0, 10] 10)
 
 syntax_consts "_Ex1" \<rightleftharpoons> Ex1
 
@@ -155,8 +155,8 @@
 
 
 syntax
-  "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3\<nexists>_./ _)\<close> [0, 10] 10)
-  "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(3\<nexists>!_./ _)\<close> [0, 10] 10)
+  "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<nexists>\<close>\<close>\<nexists>_./ _)\<close> [0, 10] 10)
+  "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<nexists>!\<close>\<close>\<nexists>!_./ _)\<close> [0, 10] 10)
 syntax_consts
   "_Not_Ex" \<rightleftharpoons> Ex and
   "_Not_Ex1" \<rightleftharpoons> Ex1
@@ -179,7 +179,7 @@
   iff :: "[bool, bool] \<Rightarrow> bool"  (infixr \<open>\<longleftrightarrow>\<close> 25)
   where "A \<longleftrightarrow> B \<equiv> A = B"
 
-syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  (\<open>(3THE _./ _)\<close> [0, 10] 10)
+syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder THE\<close>\<close>THE _./ _)\<close> [0, 10] 10)
 syntax_consts "_The" \<rightleftharpoons> The
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
 print_translation \<open>
@@ -190,12 +190,12 @@
 
 nonterminal case_syn and cases_syn
 syntax
-  "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  (\<open>(case _ of/ _)\<close> 10)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(2_ \<Rightarrow>/ _)\<close> 10)
+  "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>mixfix case expression\<close>\<close>case _ of/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  (\<open>_\<close>)
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  (\<open>_/ | _\<close>)
 syntax (ASCII)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(2_ =>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ =>/ _)\<close> 10)
 
 notation (ASCII)
   All  (binder \<open>ALL \<close> 10) and
@@ -224,7 +224,7 @@
 
   True_or_False: "(P = True) \<or> (P = False)"
 
-definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(if (_)/ then (_)/ else (_))\<close> [0, 0, 10] 10)
+definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>mixfix if expression\<close>\<close>if (_)/ then (_)/ else (_))\<close> [0, 0, 10] 10)
   where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
 
 definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
@@ -232,10 +232,10 @@
 
 nonterminal letbinds and letbind
 syntax
-  "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              (\<open>(2_ =/ _)\<close> 10)
+  "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              (\<open>(\<open>indent=2 notation=\<open>mixfix let binding\<close>\<close>_ =/ _)\<close> 10)
   ""            :: "letbind \<Rightarrow> letbinds"                 (\<open>_\<close>)
   "_binds"      :: "[letbind, letbinds] \<Rightarrow> letbinds"     (\<open>_;/ _\<close>)
-  "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                (\<open>(let (_)/ in (_))\<close> [0, 10] 10)
+  "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                (\<open>(\<open>notation=\<open>mixfix let expression\<close>\<close>let (_)/ in (_))\<close> [0, 10] 10)
 syntax_consts
   "_bind" "_binds" "_Let" \<rightleftharpoons> Let
 translations
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -17,11 +17,11 @@
   where someI: "P x \<Longrightarrow> P (Eps P)"
 
 syntax (epsilon)
-  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  (\<open>(3\<some>_./ _)\<close> [0, 10] 10)
+  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder \<some>\<close>\<close>\<some>_./ _)\<close> [0, 10] 10)
 syntax (input)
-  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  (\<open>(3@ _./ _)\<close> [0, 10] 10)
+  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder @\<close>\<close>@ _./ _)\<close> [0, 10] 10)
 syntax
-  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  (\<open>(3SOME _./ _)\<close> [0, 10] 10)
+  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder SOME\<close>\<close>SOME _./ _)\<close> [0, 10] 10)
 
 syntax_consts "_Eps" \<rightleftharpoons> Eps
 
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Inductive.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -525,9 +525,9 @@
 
 text \<open>Lambda-abstractions with pattern matching:\<close>
 syntax (ASCII)
-  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  (\<open>(%_)\<close> 10)
+  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  (\<open>(\<open>notation=abstraction\<close>%_)\<close> 10)
 syntax
-  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  (\<open>(\<lambda>_)\<close> 10)
+  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  (\<open>(\<open>notation=abstraction\<close>\<lambda>_)\<close> 10)
 parse_translation \<open>
   let
     fun fun_tr ctxt [cs] =
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Lattices_Big.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -465,10 +465,10 @@
 end
 
 syntax
-  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3MIN _./ _)\<close> [0, 10] 10)
-  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3MIN _\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3MAX _./ _)\<close> [0, 10] 10)
-  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3MAX _\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder MIN\<close>\<close>MIN _./ _)\<close> [0, 10] 10)
+  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder MIN\<close>\<close>MIN _\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder MAX\<close>\<close>MAX _./ _)\<close> [0, 10] 10)
+  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder MAX\<close>\<close>MAX _\<in>_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_MIN1" "_MIN" \<rightleftharpoons> Min and
@@ -923,7 +923,7 @@
 
 syntax
   "_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
-    (\<open>(3ARG'_MIN _ _./ _)\<close> [1000, 0, 10] 10)
+    (\<open>(\<open>indent=3 notation=\<open>binder ARG_MIN\<close>\<close>ARG'_MIN _ _./ _)\<close> [1000, 0, 10] 10)
 syntax_consts
   "_arg_min" \<rightleftharpoons> arg_min
 translations
@@ -1034,7 +1034,7 @@
 
 syntax
   "_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
-    (\<open>(3ARG'_MAX _ _./ _)\<close> [1000, 0, 10] 10)
+    (\<open>(\<open>indent=3 notation=\<open>binder ARG_MAX\<close>\<close>ARG'_MAX _ _./ _)\<close> [1000, 0, 10] 10)
 syntax_consts
   "_arg_max" \<rightleftharpoons> arg_max
 translations
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/List.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -86,9 +86,9 @@
 
 text \<open>Special input syntax for filter:\<close>
 syntax (ASCII)
-  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  (\<open>(1[_<-_./ _])\<close>)
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix filter\<close>\<close>[_<-_./ _])\<close>)
 syntax
-  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  (\<open>(1[_\<leftarrow>_ ./ _])\<close>)
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix filter\<close>\<close>[_\<leftarrow>_ ./ _])\<close>)
 syntax_consts
   "_filter" \<rightleftharpoons> filter
 translations
@@ -135,7 +135,7 @@
 nonterminal lupdbinds and lupdbind
 
 syntax
-  "_lupdbind":: "['a, 'a] => lupdbind"    (\<open>(2_ :=/ _)\<close>)
+  "_lupdbind":: "['a, 'a] => lupdbind"    (\<open>(\<open>indent=2 notation=\<open>mixfix list update\<close>\<close>_ :=/ _)\<close>)
   "" :: "lupdbind => lupdbinds"    (\<open>_\<close>)
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    (\<open>_,/ _\<close>)
   "_LUpdate" :: "['a, lupdbinds] => 'a"    (\<open>_/[(_)]\<close> [1000,0] 900)
@@ -175,7 +175,7 @@
 "product_lists [] = [[]]" |
 "product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)"
 
-primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" (\<open>(1[_..</_'])\<close>) where
+primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" (\<open>(\<open>indent=1 notation=\<open>mixfix list interval\<close>\<close>[_..</_'])\<close>) where
 upt_0: "[i..<0] = []" |
 upt_Suc: "[i..<(Suc j)] = (if i \<le> j then [i..<j] @ [j] else [])"
 
@@ -3432,7 +3432,7 @@
 
 subsubsection \<open>\<open>upto\<close>: interval-list on \<^typ>\<open>int\<close>\<close>
 
-function upto :: "int \<Rightarrow> int \<Rightarrow> int list" (\<open>(1[_../_])\<close>) where
+function upto :: "int \<Rightarrow> int \<Rightarrow> int list" (\<open>(\<open>indent=1 notation=\<open>mixfix list interval\<close>\<close>[_../_])\<close>) where
   "upto i j = (if i \<le> j then i # [i+1..j] else [])"
 by auto
 termination
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Main.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -77,10 +77,10 @@
   Sup  (\<open>\<Squnion> _\<close> [900] 900)
 
 syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 end
 
@@ -96,10 +96,10 @@
   Sup  (\<open>\<Squnion> _\<close> [900] 900)
 
 no_syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 end
 
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Map.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -61,7 +61,7 @@
   ""         :: "maplet \<Rightarrow> updbind"              (\<open>_\<close>)
   ""         :: "maplet \<Rightarrow> maplets"             (\<open>_\<close>)
   "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>)
-  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(1[_])\<close>)
+  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)
 
 syntax (ASCII)
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Orderings.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -179,9 +179,9 @@
 
 notation
   less_eq  (\<open>'(\<le>')\<close>) and
-  less_eq  (\<open>(_/ \<le> _)\<close>  [51, 51] 50) and
+  less_eq  (\<open>(\<open>notation=\<open>infix \<le>\<close>\<close>_/ \<le> _)\<close>  [51, 51] 50) and
   less  (\<open>'(<')\<close>) and
-  less  (\<open>(_/ < _)\<close>  [51, 51] 50)
+  less  (\<open>(\<open>notation=\<open>infix <\<close>\<close>_/ < _)\<close>  [51, 51] 50)
 
 abbreviation (input)
   greater_eq  (infix \<open>\<ge>\<close> 50)
@@ -193,7 +193,7 @@
 
 notation (ASCII)
   less_eq  (\<open>'(<=')\<close>) and
-  less_eq  (\<open>(_/ <= _)\<close> [51, 51] 50)
+  less_eq  (\<open>(\<open>notation=\<open>infix <=\<close>\<close>_/ <= _)\<close> [51, 51] 50)
 
 notation (input)
   greater_eq  (infix \<open>>=\<close> 50)
@@ -710,40 +710,40 @@
 subsection \<open>Bounded quantifiers\<close>
 
 syntax (ASCII)
-  "_All_less" :: "[idt, 'a, bool] => bool"    (\<open>(3ALL _<_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_less" :: "[idt, 'a, bool] => bool"    (\<open>(3EX _<_./ _)\<close>  [0, 0, 10] 10)
-  "_All_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3ALL _<=_./ _)\<close> [0, 0, 10] 10)
-  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3EX _<=_./ _)\<close> [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<_./ _)\<close>  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<=_./ _)\<close> [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<=_./ _)\<close> [0, 0, 10] 10)
 
-  "_All_greater" :: "[idt, 'a, bool] => bool"    (\<open>(3ALL _>_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_greater" :: "[idt, 'a, bool] => bool"    (\<open>(3EX _>_./ _)\<close>  [0, 0, 10] 10)
-  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3ALL _>=_./ _)\<close> [0, 0, 10] 10)
-  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3EX _>=_./ _)\<close> [0, 0, 10] 10)
+  "_All_greater" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _>_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_greater" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _>_./ _)\<close>  [0, 0, 10] 10)
+  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _>=_./ _)\<close> [0, 0, 10] 10)
+  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _>=_./ _)\<close> [0, 0, 10] 10)
 
-  "_All_neq" :: "[idt, 'a, bool] => bool"    (\<open>(3ALL _~=_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_neq" :: "[idt, 'a, bool] => bool"    (\<open>(3EX _~=_./ _)\<close>  [0, 0, 10] 10)
+  "_All_neq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _~=_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_neq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _~=_./ _)\<close>  [0, 0, 10] 10)
 
 syntax
-  "_All_less" :: "[idt, 'a, bool] => bool"    (\<open>(3\<forall>_<_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_less" :: "[idt, 'a, bool] => bool"    (\<open>(3\<exists>_<_./ _)\<close>  [0, 0, 10] 10)
-  "_All_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3\<forall>_\<le>_./ _)\<close> [0, 0, 10] 10)
-  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3\<exists>_\<le>_./ _)\<close> [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_<_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_<_./ _)\<close>  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<le>_./ _)\<close> [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<le>_./ _)\<close> [0, 0, 10] 10)
 
-  "_All_greater" :: "[idt, 'a, bool] => bool"    (\<open>(3\<forall>_>_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_greater" :: "[idt, 'a, bool] => bool"    (\<open>(3\<exists>_>_./ _)\<close>  [0, 0, 10] 10)
-  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3\<forall>_\<ge>_./ _)\<close> [0, 0, 10] 10)
-  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3\<exists>_\<ge>_./ _)\<close> [0, 0, 10] 10)
+  "_All_greater" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_>_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_greater" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_>_./ _)\<close>  [0, 0, 10] 10)
+  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<ge>_./ _)\<close> [0, 0, 10] 10)
+  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<ge>_./ _)\<close> [0, 0, 10] 10)
 
-  "_All_neq" :: "[idt, 'a, bool] => bool"    (\<open>(3\<forall>_\<noteq>_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_neq" :: "[idt, 'a, bool] => bool"    (\<open>(3\<exists>_\<noteq>_./ _)\<close>  [0, 0, 10] 10)
+  "_All_neq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<noteq>_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_neq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<noteq>_./ _)\<close>  [0, 0, 10] 10)
 
 syntax (input)
-  "_All_less" :: "[idt, 'a, bool] => bool"    (\<open>(3! _<_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_less" :: "[idt, 'a, bool] => bool"    (\<open>(3? _<_./ _)\<close>  [0, 0, 10] 10)
-  "_All_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3! _<=_./ _)\<close> [0, 0, 10] 10)
-  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(3? _<=_./ _)\<close> [0, 0, 10] 10)
-  "_All_neq" :: "[idt, 'a, bool] => bool"    (\<open>(3! _~=_./ _)\<close>  [0, 0, 10] 10)
-  "_Ex_neq" :: "[idt, 'a, bool] => bool"    (\<open>(3? _~=_./ _)\<close>  [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder !\<close>\<close>! _<_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ?\<close>\<close>? _<_./ _)\<close>  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder !\<close>\<close>! _<=_./ _)\<close> [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ?\<close>\<close>? _<=_./ _)\<close> [0, 0, 10] 10)
+  "_All_neq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder !\<close>\<close>! _~=_./ _)\<close>  [0, 0, 10] 10)
+  "_Ex_neq" :: "[idt, 'a, bool] => bool"    (\<open>(\<open>indent=3 notation=\<open>binder ?\<close>\<close>? _~=_./ _)\<close>  [0, 0, 10] 10)
 
 syntax_consts
   "_All_less" "_All_less_eq" "_All_greater" "_All_greater_eq" "_All_neq" \<rightleftharpoons> All and
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Power.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -23,7 +23,7 @@
   power (\<open>(_\<^bsup>_\<^esup>)\<close> [1000] 1000)
 
 text \<open>Special syntax for squares.\<close>
-abbreviation power2 :: "'a \<Rightarrow> 'a"  (\<open>(_\<^sup>2)\<close> [1000] 999)
+abbreviation power2 :: "'a \<Rightarrow> 'a"  (\<open>(\<open>notation=\<open>postfix 2\<close>\<close>_\<^sup>2)\<close> [1000] 999)
   where "x\<^sup>2 \<equiv> x ^ 2"
 
 end
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Product_Type.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -214,7 +214,7 @@
 
 definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
 
-typedef ('a, 'b) prod (\<open>(_ \<times>/ _)\<close> [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod (\<open>(\<open>notation=\<open>infix \<times>\<close>\<close>_ \<times>/ _)\<close> [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
   unfolding prod_def by auto
 
 type_notation (ASCII)
@@ -286,7 +286,7 @@
 
 nonterminal tuple_args and patterns
 syntax
-  "_tuple"      :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b"        (\<open>(1'(_,/ _'))\<close>)
+  "_tuple"      :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b"        (\<open>(\<open>indent=1 notation=\<open>mixfix tuple\<close>\<close>'(_,/ _'))\<close>)
   "_tuple_arg"  :: "'a \<Rightarrow> tuple_args"                   (\<open>_\<close>)
   "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args"     (\<open>_,/ _\<close>)
   "_pattern"    :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn"         (\<open>'(_,/ _')\<close>)
@@ -1013,7 +1013,8 @@
 end
 
 syntax
-  "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (\<open>(3SIGMA _:_./ _)\<close> [0, 0, 10] 10)
+  "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
+    (\<open>(\<open>indent=3 notation=\<open>binder SIGMA\<close>\<close>SIGMA _:_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_Sigma" \<rightleftharpoons> Sigma
 translations
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Record.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -426,29 +426,29 @@
   "_constify"           :: "id => ident"                        (\<open>_\<close>)
   "_constify"           :: "longid => ident"                    (\<open>_\<close>)
 
-  "_field_type"         :: "ident => type => field_type"        (\<open>(2_ ::/ _)\<close>)
+  "_field_type"         :: "ident => type => field_type"        (\<open>(\<open>indent=2 notation=\<open>infix field type\<close>\<close>_ ::/ _)\<close>)
   ""                    :: "field_type => field_types"          (\<open>_\<close>)
   "_field_types"        :: "field_type => field_types => field_types"    (\<open>_,/ _\<close>)
-  "_record_type"        :: "field_types => type"                (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
+  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
 
-  "_field"              :: "ident => 'a => field"               (\<open>(2_ =/ _)\<close>)
+  "_field"              :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
   ""                    :: "field => fields"                    (\<open>_\<close>)
   "_fields"             :: "field => fields => fields"          (\<open>_,/ _\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
+  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
 
-  "_field_update"       :: "ident => 'a => field_update"        (\<open>(2_ :=/ _)\<close>)
+  "_field_update"       :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
   ""                    :: "field_update => field_updates"      (\<open>_\<close>)
   "_field_updates"      :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
 
 syntax (ASCII)
-  "_record_type"        :: "field_types => type"                (\<open>(3'(| _ |'))\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(3'(| _,/ (2... ::/ _) |'))\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(3'(| _ |'))\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
+  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _ |'))\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (2... ::/ _) |'))\<close>)
+  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _ |'))\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (2... =/ _) |'))\<close>)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
 
 
 subsection \<open>Record package\<close>
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Relation.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -1074,15 +1074,15 @@
 
 subsubsection \<open>Converse\<close>
 
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  (\<open>(_\<inverse>)\<close> [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999)
   for r :: "('a \<times> 'b) set"
   where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
 
-notation conversep  (\<open>(_\<inverse>\<inverse>)\<close> [1000] 1000)
+notation conversep  (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
 
 notation (ASCII)
-  converse  (\<open>(_^-1)\<close> [1000] 999) and
-  conversep (\<open>(_^--1)\<close> [1000] 1000)
+  converse  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_^-1)\<close> [1000] 999) and
+  conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_^--1)\<close> [1000] 1000)
 
 lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
   by (fact converse.intros)
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
 
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -29,35 +29,35 @@
 begin
 
 definition
-  lessThan    :: "'a => 'a set" (\<open>(1{..<_})\<close>) where
+  lessThan    :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{..<_})\<close>) where
   "{..<u} == {x. x < u}"
 
 definition
-  atMost      :: "'a => 'a set" (\<open>(1{.._})\<close>) where
+  atMost      :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{.._})\<close>) where
   "{..u} == {x. x \<le> u}"
 
 definition
-  greaterThan :: "'a => 'a set" (\<open>(1{_<..})\<close>) where
+  greaterThan :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..})\<close>) where
   "{l<..} == {x. l<x}"
 
 definition
-  atLeast     :: "'a => 'a set" (\<open>(1{_..})\<close>) where
+  atLeast     :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..})\<close>) where
   "{l..} == {x. l\<le>x}"
 
 definition
-  greaterThanLessThan :: "'a => 'a => 'a set"  (\<open>(1{_<..<_})\<close>) where
+  greaterThanLessThan :: "'a => 'a => 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..<_})\<close>) where
   "{l<..<u} == {l<..} Int {..<u}"
 
 definition
-  atLeastLessThan :: "'a => 'a => 'a set"      (\<open>(1{_..<_})\<close>) where
+  atLeastLessThan :: "'a => 'a => 'a set"      (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..<_})\<close>) where
   "{l..<u} == {l..} Int {..<u}"
 
 definition
-  greaterThanAtMost :: "'a => 'a => 'a set"    (\<open>(1{_<.._})\<close>) where
+  greaterThanAtMost :: "'a => 'a => 'a set"    (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<.._})\<close>) where
   "{l<..u} == {l<..} Int {..u}"
 
 definition
-  atLeastAtMost :: "'a => 'a => 'a set"        (\<open>(1{_.._})\<close>) where
+  atLeastAtMost :: "'a => 'a => 'a set"        (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_.._})\<close>) where
   "{l..u} == {l..} Int {..u}"
 
 end
@@ -67,10 +67,10 @@
 \<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close>
 
 syntax (ASCII)
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3UN _<=_./ _)\<close> [0, 0, 10] 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3UN _<_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3INT _<=_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3INT _<_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<=_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<=_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<_./ _)\<close> [0, 0, 10] 10)
 
 syntax (latex output)
   "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       (\<open>(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
@@ -79,10 +79,10 @@
   "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       (\<open>(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Union>_<_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(3\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_<_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
@@ -1988,10 +1988,10 @@
 subsection \<open>Summation indexed over intervals\<close>
 
 syntax (ASCII)
-  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _<_./ _)\<close> [0,0,10] 10)
-  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(SUM _<=_./ _)\<close> [0,0,10] 10)
+  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<_./ _)\<close> [0,0,10] 10)
+  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<=_./ _)\<close> [0,0,10] 10)
 
 syntax (latex_sum output)
   "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2004,10 +2004,10 @@
  (\<open>(3\<^latex>\<open>$\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
 
 syntax
-  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_<_./ _)\<close> [0,0,10] 10)
-  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
+  "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_<_./ _)\<close> [0,0,10] 10)
+  "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
 
 syntax_consts
   "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
@@ -2681,10 +2681,10 @@
 subsection \<open>Products indexed over intervals\<close>
 
 syntax (ASCII)
-  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _<_./ _)\<close> [0,0,10] 10)
-  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(PROD _<=_./ _)\<close> [0,0,10] 10)
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<_./ _)\<close> [0,0,10] 10)
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<=_./ _)\<close> [0,0,10] 10)
 
 syntax (latex_prod output)
   "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2697,10 +2697,10 @@
  (\<open>(3\<^latex>\<open>$\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
 
 syntax
-  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
-  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
-  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_<_./ _)\<close> [0,0,10] 10)
-  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(3\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_<_./ _)\<close> [0,0,10] 10)
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
 
 syntax_consts
   "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -1191,7 +1191,7 @@
 subsection \<open>Limits on sequences\<close>
 
 abbreviation (in topological_space)
-  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"  (\<open>((_)/ \<longlonglongrightarrow> (_))\<close> [60, 60] 60)
+  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"  (\<open>(\<open>notation=\<open>infix LIMSEQ\<close>\<close>(_)/ \<longlonglongrightarrow> (_))\<close> [60, 60] 60)
   where "X \<longlonglongrightarrow> L \<equiv> (X \<longlongrightarrow> L) sequentially"
 
 abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a"
@@ -1760,7 +1760,7 @@
 subsection \<open>Function limit at a point\<close>
 
 abbreviation LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
-    (\<open>((_)/ \<midarrow>(_)/\<rightarrow> (_))\<close> [60, 0, 60] 60)
+    (\<open>(\<open>notation=\<open>infix LIM\<close>\<close>(_)/ \<midarrow>(_)/\<rightarrow> (_))\<close> [60, 0, 60] 60)
   where "f \<midarrow>a\<rightarrow> L \<equiv> (f \<longlongrightarrow> L) (at a)"
 
 lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -26,21 +26,21 @@
 context notes [[inductive_internals]]
 begin
 
-inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(_\<^sup>*)\<close> [1000] 999)
+inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999)
   for r :: "('a \<times> 'a) set"
   where
     rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
   | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
 
-inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(_\<^sup>+)\<close> [1000] 999)
+inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999)
   for r :: "('a \<times> 'a) set"
   where
     r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
   | trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
 
 notation
-  rtranclp  (\<open>(_\<^sup>*\<^sup>*)\<close> [1000] 1000) and
-  tranclp  (\<open>(_\<^sup>+\<^sup>+)\<close> [1000] 1000)
+  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000) and
+  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
 
 declare
   rtrancl_def [nitpick_unfold del]
@@ -50,19 +50,19 @@
 
 end
 
-abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(_\<^sup>=)\<close> [1000] 999)
+abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999)
   where "r\<^sup>= \<equiv> r \<union> Id"
 
-abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(_\<^sup>=\<^sup>=)\<close> [1000] 1000)
+abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
   where "r\<^sup>=\<^sup>= \<equiv> sup r (=)"
 
 notation (ASCII)
-  rtrancl  (\<open>(_^*)\<close> [1000] 999) and
-  trancl  (\<open>(_^+)\<close> [1000] 999) and
-  reflcl  (\<open>(_^=)\<close> [1000] 999) and
-  rtranclp  (\<open>(_^**)\<close> [1000] 1000) and
-  tranclp  (\<open>(_^++)\<close> [1000] 1000) and
-  reflclp  (\<open>(_^==)\<close> [1000] 1000)
+  rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
+  trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
+  reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
+  rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000) and
+  tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
+  reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
 
 
 subsection \<open>Reflexive closure\<close>
diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Typerep.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -18,7 +18,7 @@
 end
 
 syntax
-  "_TYPEREP" :: "type => logic"  (\<open>(1TYPEREP/(1'(_')))\<close>)
+  "_TYPEREP" :: "type => logic"  (\<open>(\<open>indent=1 notation=\<open>prefix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>)
 syntax_consts
   "_TYPEREP" \<rightleftharpoons> typerep