# HG changeset patch
# User wenzelm
# Date 1728509909 -7200
# Node ID 6ad2c917dd2e7ea6751b69ac9be6f2a5c8d07c63
# Parent  3e3e7a68cd80ee59d15e00308a774fd94d345c0c
more inner-syntax markup;

diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -24,7 +24,8 @@
   where "a_l_coset G = l_coset (add_monoid G)"
 
 definition
-  A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   (\<open>a'_rcosets\<index> _\<close> [81] 80)
+  A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"
+    (\<open>(\<open>open_block notation=\<open>prefix a_rcosets\<close>\<close>a'_rcosets\<index> _)\<close> [81] 80)
   where "A_RCOSETS G H = RCOSETS (add_monoid G) H"
 
 definition
@@ -32,7 +33,8 @@
   where "set_add G = set_mult (add_monoid G)"
 
 definition
-  A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  (\<open>a'_set'_inv\<index> _\<close> [81] 80)
+  A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"
+    (\<open>(\<open>open_block notation=\<open>prefix a_set_inv\<close>\<close>a'_set'_inv\<index> _)\<close> [81] 80)
   where "A_SET_INV G H = SET_INV (add_monoid G) H"
 
 definition
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Algebraic_Closure_Type.thy
--- a/src/HOL/Algebra/Algebraic_Closure_Type.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Algebraic_Closure_Type.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -468,8 +468,8 @@
 
 bundle alg_closure_syntax
 begin
-notation to_ac (\<open>_\<up>\<close> [1000] 999)
-notation of_ac (\<open>_\<down>\<close> [1000] 999)
+notation to_ac (\<open>(\<open>open_block notation=\<open>postfix \<up>\<close>\<close>_\<up>)\<close> [1000] 999)
+notation of_ac (\<open>(\<open>open_block notation=\<open>postfix \<down>\<close>\<close>_\<down>)\<close> [1000] 999)
 end
 
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Coset.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -19,7 +19,8 @@
   where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
 
 definition
-  RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   (\<open>rcosets\<index> _\<close> [81] 80)
+  RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"
+    (\<open>(\<open>open_block notation=\<open>prefix rcosets\<close>\<close>rcosets\<index> _)\<close> [81] 80)
   where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
 
 definition
@@ -27,7 +28,8 @@
   where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
 
 definition
-  SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  (\<open>set'_inv\<index> _\<close> [81] 80)
+  SET_INV :: "[_,'a set] \<Rightarrow> 'a set"
+    (\<open>(\<open>open_block notation=\<open>prefix set_inv\<close>\<close>set'_inv\<index> _)\<close> [81] 80)
   where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
 
 
@@ -659,7 +661,8 @@
 subsubsection\<open>An Equivalence Relation\<close>
 
 definition
-  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  (\<open>rcong\<index> _\<close>)
+  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
+    (\<open>(\<open>open_block notation=\<open>prefix rcong\<close>\<close>rcong\<index> _)\<close>)
   where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G \<and> y \<in> carrier G \<and> inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
 
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -1993,11 +1993,13 @@
 
 subsubsection \<open>Definitions\<close>
 
-definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  (\<open>(_ gcdof\<index> _ _)\<close> [81,81,81] 80)
+definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"
+    (\<open>(\<open>notation=\<open>mixfix gcdof\<close>\<close>_ gcdof\<index> _ _)\<close> [81,81,81] 80)
   where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
     (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
 
-definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  (\<open>(_ lcmof\<index> _ _)\<close> [81,81,81] 80)
+definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"
+    (\<open>(\<open>notation=\<open>mixfix lcmof\<close>\<close>_ lcmof\<index> _ _)\<close> [81,81,81] 80)
   where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
     (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Exact_Sequence.thy
--- a/src/HOL/Algebra/Exact_Sequence.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Exact_Sequence.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -22,7 +22,7 @@
 
 abbreviation exact_seq_arrow ::
   "('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow>  'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
-  (\<open>(3_ / \<longlongrightarrow>\<index> _)\<close> [1000, 60])
+  (\<open>(\<open>indent=3 notation=\<open>mixfix exact_seq\<close>\<close>_ / \<longlongrightarrow>\<index> _)\<close> [1000, 60])
   where "exact_seq_arrow  f t G \<equiv> (G # (fst t), f # (snd t))"
 
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -307,7 +307,7 @@
 
 syntax
   "_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
-      (\<open>(3\<Otimes>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Otimes>\<close>\<close>\<Otimes>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
 syntax_consts
   "_finprod" \<rightleftharpoons> finprod
 translations
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -22,7 +22,8 @@
   one     :: 'a (\<open>\<one>\<index>\<close>)
 
 definition
-  m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" (\<open>inv\<index> _\<close> [81] 80)
+  m_inv :: "('a, 'b) monoid_scheme => 'a => 'a"
+    (\<open>(\<open>open_block notation=\<open>prefix inv\<close>\<close>inv\<index> _)\<close> [81] 80)
   where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
 
 definition
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -45,8 +45,9 @@
 
 subsubsection (in ring) \<open>Ideals Generated by a Subset of \<^term>\<open>carrier R\<close>\<close>
 
-definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  (\<open>Idl\<index> _\<close> [80] 79)
-  where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
+definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"
+    (\<open>(\<open>open_block notation=\<open>prefix Idl\<close>\<close>Idl\<index> _)\<close> [80] 79)
+  where "Idl\<^bsub>R\<^esub> S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
 
 subsubsection \<open>Principal Ideals\<close>
 
@@ -411,8 +412,9 @@
 
 text \<open>Generation of Principal Ideals in Commutative Rings\<close>
 
-definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"  (\<open>PIdl\<index> _\<close> [80] 79)
-  where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
+definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"
+    (\<open>(\<open>open_block notation=\<open>prefix PIdl\<close>\<close>PIdl\<index> _)\<close> [80] 79)
+  where "PIdl\<^bsub>R\<^esub> a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
 
 text \<open>genhideal (?) really generates an ideal\<close>
 lemma (in cring) cgenideal_ideal:
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Indexed_Polynomials.thy
--- a/src/HOL/Algebra/Indexed_Polynomials.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -38,7 +38,8 @@
 definition (in ring) carrier_coeff :: "('c multiset \<Rightarrow> 'a) \<Rightarrow> bool"
   where "carrier_coeff P \<longleftrightarrow> (\<forall>m. P m \<in> carrier R)"
 
-inductive_set (in ring) indexed_pset :: "'c set \<Rightarrow> 'a set \<Rightarrow> ('c multiset \<Rightarrow> 'a) set" (\<open>_ [\<X>\<index>]\<close> 80)
+inductive_set (in ring) indexed_pset :: "'c set \<Rightarrow> 'a set \<Rightarrow> ('c multiset \<Rightarrow> 'a) set"
+  (\<open>(\<open>open_block notation=\<open>postfix \<X>\<close>\<close>_ [\<X>\<index>])\<close> 80)
   for I and K where
     indexed_const:  "k \<in> K \<Longrightarrow> indexed_const k \<in> (K[\<X>\<^bsub>I\<^esub>])"
   | indexed_padd:  "\<lbrakk> P \<in> (K[\<X>\<^bsub>I\<^esub>]); Q \<in> (K[\<X>\<^bsub>I\<^esub>]) \<rbrakk> \<Longrightarrow> P \<Oplus> Q \<in> (K[\<X>\<^bsub>I\<^esub>])"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -15,11 +15,11 @@
 subsection \<open>Supremum and infimum\<close>
 
 definition
-  sup :: "[_, 'a set] => 'a" (\<open>\<Squnion>\<index>_\<close> [90] 90)
+  sup :: "[_, 'a set] => 'a" (\<open>(\<open>open_block notation=\<open>prefix \<Squnion>\<close>\<close>\<Squnion>\<index>_)\<close> [90] 90)
   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
 
 definition
-  inf :: "[_, 'a set] => 'a" (\<open>\<Sqinter>\<index>_\<close> [90] 90)
+  inf :: "[_, 'a set] => 'a" (\<open>(\<open>open_block notation=\<open>prefix \<Sqinter>\<close>\<close>\<Sqinter>\<index>_)\<close> [90] 90)
   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
 
 definition supr :: 
@@ -31,15 +31,17 @@
   where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
 
 syntax
-  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3IINF\<index> _./ _)\<close> [0, 10] 10)
-  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3IINF\<index> _:_./ _)\<close> [0, 0, 10] 10)
-  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3SSUP\<index> _./ _)\<close> [0, 10] 10)
-  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3SSUP\<index> _:_./ _)\<close> [0, 0, 10] 10)
-
+  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder IINF\<close>\<close>IINF\<index> _./ _)\<close> [0, 10] 10)
+  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder IINF\<close>\<close>IINF\<index> _:_./ _)\<close> [0, 0, 10] 10)
+  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder SSUP\<close>\<close>SSUP\<index> _./ _)\<close> [0, 10] 10)
+  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"
+    (\<open>(\<open>indent=3 notation=\<open>binder SSUP\<close>\<close>SSUP\<index> _:_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_inf1" "_inf" == infi and
   "_sup1" "_sup" == supr
-
 translations
   "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
   "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Left_Coset.thy
--- a/src/HOL/Algebra/Left_Coset.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Left_Coset.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -7,7 +7,8 @@
 begin
 
 definition
-  LCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   (\<open>lcosets\<index> _\<close> [81] 80)
+  LCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"
+    (\<open>(\<open>open_block notation=\<open>prefix lcosets\<close>\<close>lcosets\<index> _)\<close> [81] 80)
   where "lcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {a <#\<^bsub>G\<^esub> H})"
 
 definition
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Order.thy
--- a/src/HOL/Algebra/Order.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Order.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -411,7 +411,8 @@
 subsubsection \<open>Intervals\<close>
 
 definition
-  at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set" (\<open>(1\<lbrace>_.._\<rbrace>\<index>)\<close>)
+  at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix interval\<close>\<close>\<lbrace>_.._\<rbrace>\<index>)\<close>)
   where "\<lbrace>l..u\<rbrace>\<^bsub>A\<^esub> = {x \<in> carrier A. l \<sqsubseteq>\<^bsub>A\<^esub> x \<and> x \<sqsubseteq>\<^bsub>A\<^esub> u}"
 
 context weak_partial_order
@@ -452,8 +453,9 @@
   shows "isotone L1 L2 f"
   using assms by (auto simp add:isotone_def)
 
-abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" (\<open>Mono\<index>\<close>)
-  where "Monotone L f \<equiv> isotone L L f"
+abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>prefix Mono\<close>\<close>Mono\<index>)\<close>)
+  where "Mono\<^bsub>L\<^esub> f \<equiv> isotone L L f"
 
 lemma use_iso1:
   "\<lbrakk>isotone A A f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
@@ -478,8 +480,9 @@
 subsubsection \<open>Idempotent functions\<close>
 
 definition idempotent :: 
-  "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" (\<open>Idem\<index>\<close>) where
-  "idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
+  "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>prefix Idem\<close>\<close>Idem\<index>)\<close>)
+  where "Idem\<^bsub>L\<^esub> f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
 
 lemma (in weak_partial_order) idempotent:
   "\<lbrakk>Idem f; x \<in> carrier L\<rbrakk> \<Longrightarrow> f (f x) .= f x"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Polynomials.thy
--- a/src/HOL/Algebra/Polynomials.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Polynomials.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -1359,7 +1359,8 @@
 
 subsection \<open>Algebraic Structure of Polynomials\<close>
 
-definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring" (\<open>_ [X]\<index>\<close> 80)
+definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring"
+    (\<open>(\<open>open_block notation=\<open>postfix X\<close>\<close>_ [X]\<index>)\<close> 80)
   where "univ_poly R K =
            \<lparr> carrier = { p. polynomial\<^bsub>R\<^esub> K p },
                 mult = ring.poly_mult R,
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -12,7 +12,7 @@
 subsection \<open>Multiplication on Cosets\<close>
 
 definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
-    (\<open>[mod _:] _ \<Otimes>\<index> _\<close> [81,81,81] 80)
+    (\<open>(\<open>open_block notation=\<open>mixfix rcoset_mult\<close>\<close>[mod _:] _ \<Otimes>\<index> _)\<close> [81,81,81] 80)
   where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
 
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Ring.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -23,16 +23,17 @@
 text \<open>Derived operations.\<close>
 
 definition
-  a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" (\<open>\<ominus>\<index> _\<close> [81] 80)
+  a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" (\<open>(\<open>open_block notation=\<open>prefix \<ominus>\<close>\<close>\<ominus>\<index> _)\<close> [81] 80)
   where "a_inv R = m_inv (add_monoid R)"
 
 definition
-  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (\<open>(_ \<ominus>\<index> _)\<close> [65,66] 65)
+  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (\<open>(\<open>notation=\<open>infix \<ominus>\<close>\<close>_ \<ominus>\<index> _)\<close> [65,66] 65)
   where "x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 definition
-  add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a" (\<open>[_] \<cdot>\<index> _\<close> [81, 81] 80)
-  where "add_pow R k a = pow (add_monoid R) a k"
+  add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a"
+    (\<open>(\<open>open_block notation=\<open>mixfix \<cdot>\<close>\<close>[_] \<cdot>\<index> _)\<close> [81, 81] 80)
+  where "[k] \<cdot>\<^bsub>R\<^esub> a = pow (add_monoid R) a k"
 
 locale abelian_monoid =
   fixes G (structure)
@@ -45,7 +46,7 @@
 
 syntax
   "_finsum" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
-      (\<open>(3\<Oplus>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Oplus>\<close>\<close>\<Oplus>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
 syntax_consts
   "_finsum" \<rightleftharpoons> finsum
 translations
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -33,7 +33,7 @@
   assumes euclidean_all_zero_iff:
     "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
 
-syntax "_type_dimension" :: "type \<Rightarrow> nat"  (\<open>(1DIM/(1'(_')))\<close>)
+syntax "_type_dimension" :: "type \<Rightarrow> nat"  (\<open>(\<open>indent=1 notation=\<open>mixfix type dimension\<close>\<close>DIM/(1'(_')))\<close>)
 syntax_consts "_type_dimension" \<rightleftharpoons> card
 translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
 typed_print_translation \<open>
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -14,7 +14,8 @@
 
 open_bundle lipschitz_syntax
 begin
-notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
+notation\<^marker>\<open>tag important\<close>
+  lipschitz_on (\<open>(\<open>open_block notation=\<open>postfix lipschitz_on\<close>\<close>_-lipschitz'_on)\<close> [1000])
 end
 
 lemma lipschitz_onI: "L-lipschitz_on X f"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -1004,11 +1004,10 @@
   "almost_everywhere M P \<equiv> eventually P (ae_filter M)"
 
 syntax
-  "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" (\<open>AE _ in _. _\<close> [0,0,10] 10)
-
+  "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>binder AE\<close>\<close>AE _ in _. _)\<close> [0,0,10] 10)
 syntax_consts
   "_almost_everywhere" \<rightleftharpoons> almost_everywhere
-
 translations
   "AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
 
@@ -1017,11 +1016,9 @@
 
 syntax
   "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
-  (\<open>AE _\<in>_ in _./ _\<close> [0,0,0,10] 10)
-
+    (\<open>(\<open>open_block notation=\<open>binder AE\<close>\<close>AE _\<in>_ in _./ _)\<close> [0,0,0,10] 10)
 syntax_consts
   "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
-
 translations
   "AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -584,11 +584,10 @@
   "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
 
 syntax
-  "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>\<integral>\<^sup>S _. _ \<partial>_\<close> [60,61] 110)
-
+  "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal"
+    (\<open>(\<open>open_block notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>S _. _ \<partial>_)\<close> [60,61] 110)
 syntax_consts
   "_simple_integral" == simple_integral
-
 translations
   "\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -577,21 +577,17 @@
 
 syntax
   "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
- (\<open>\<integral>\<^sup>C _. _ \<partial>_\<close> [0,0] 110)
-
+ (\<open>(\<open>open_block notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>C _. _ \<partial>_)\<close> [0,0] 110)
 syntax_consts
   "_complex_lebesgue_integral" == complex_lebesgue_integral
-
 translations
   "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
 
 syntax
   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   (\<open>(\<open>indent=3 notation=\<open>binder CLINT\<close>\<close>CLINT _|_. _)\<close> [0,0,10] 10)
-
 syntax_consts
   "_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
-
 translations
   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
 
@@ -646,19 +642,16 @@
 abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
 
 syntax
-"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
-
-"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
-
+  "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
+    (\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+  "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
+    (\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
 syntax_consts
-"_set_nn_integral" == set_nn_integral and
-"_set_lebesgue_integral" == set_lebesgue_integral
-
+  "_set_nn_integral" == set_nn_integral and
+  "_set_lebesgue_integral" == set_lebesgue_integral
 translations
-"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
-"\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+  "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
+  "\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
 lemma set_nn_integral_cong:
   assumes "M = M'" "A = B" "\<And>x. x \<in> space M \<inter> A \<Longrightarrow> f x = g x"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -6414,7 +6414,7 @@
 
 subsection\<open>Orthogonal complement\<close>
 
-definition\<^marker>\<open>tag important\<close> orthogonal_comp (\<open>_\<^sup>\<bottom>\<close> [80] 80)
+definition\<^marker>\<open>tag important\<close> orthogonal_comp (\<open>(\<open>open_block notation=\<open>postfix \<bottom>\<close>\<close>_\<^sup>\<bottom>)\<close> [80] 80)
   where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
 
 proposition subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Cardinality.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -30,7 +30,7 @@
 
 subsection \<open>Cardinalities of types\<close>
 
-syntax "_type_card" :: "type => nat" (\<open>(1CARD/(1'(_')))\<close>)
+syntax "_type_card" :: "type => nat"  (\<open>(\<open>indent=1 notation=\<open>mixfix CARD\<close>\<close>CARD/(1'(_')))\<close>)
 
 syntax_consts "_type_card" == card
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -28,8 +28,10 @@
 end
 
 syntax
-  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (\<open>(3\<Pi> _\<in>_./ _)\<close>   10)
-  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  (\<open>(3\<lambda>_\<in>_./ _)\<close> [0,0,3] 3)
+  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<in>\<close>\<close>\<Pi> _\<in>_./ _)\<close> 10)
+  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<lambda>\<in>\<close>\<close>\<lambda>_\<in>_./ _)\<close> [0, 0, 3] 3)
 syntax_consts
   "_Pi" \<rightleftharpoons> Pi and
   "_lam" \<rightleftharpoons> restrict
@@ -350,7 +352,8 @@
 abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
 
 syntax
-  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (\<open>(3\<Pi>\<^sub>E _\<in>_./ _)\<close> 10)
+  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>E\<in>\<close>\<close>\<Pi>\<^sub>E _\<in>_./ _)\<close> 10)
 syntax_consts
   "_PiE" \<rightleftharpoons> Pi\<^sub>E
 translations
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Going_To_Filter.thy
--- a/src/HOL/Library/Going_To_Filter.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Going_To_Filter.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -12,8 +12,8 @@
 begin
 
 definition going_to_within :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a set \<Rightarrow> 'a filter"
-  (\<open>(_)/ going'_to (_)/ within (_)\<close> [1000,60,60] 60) where
-  "f going_to F within A = inf (filtercomap f F) (principal A)"
+    (\<open>(\<open>open_block notation=\<open>mixfix going_to_within\<close>\<close>(_)/ going'_to (_)/ within (_))\<close> [1000,60,60] 60)
+  where "f going_to F within A = inf (filtercomap f F) (principal A)"
 
 abbreviation going_to :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter"
     (infix \<open>going'_to\<close> 60)
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -199,9 +199,9 @@
 end
 
 syntax (ASCII)
-  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    (\<open>(3SUM _. _)\<close> [0, 10] 10)
+  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _. _)\<close> [0, 10] 10)
 syntax
-  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    (\<open>(3\<Sum>_. _)\<close> [0, 10] 10)
+  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_. _)\<close> [0, 10] 10)
 syntax_consts
   "_Sum_any" \<rightleftharpoons> Sum_any
 translations
@@ -254,9 +254,9 @@
 end
 
 syntax (ASCII)
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  (\<open>(3PROD _. _)\<close> [0, 10] 10)
+  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  (\<open>(\<open>indent=4 notation=\<open>binder PROD\<close>\<close>PROD _. _)\<close> [0, 10] 10)
 syntax
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  (\<open>(3\<Prod>_. _)\<close> [0, 10] 10)
+  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  (\<open>(\<open>indent=2 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_. _)\<close> [0, 10] 10)
 syntax_consts
   "_Prod_any" == Prod_any
 translations
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Interval.thy
--- a/src/HOL/Library/Interval.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Interval.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -204,7 +204,7 @@
 
 subsection \<open>Membership\<close>
 
-abbreviation (in preorder) in_interval (\<open>(_/ \<in>\<^sub>i _)\<close> [51, 51] 50)
+abbreviation (in preorder) in_interval (\<open>(\<open>notation=\<open>infix \<in>\<^sub>i\<close>\<close>_/ \<in>\<^sub>i _)\<close> [51, 51] 50)
   where "in_interval x X \<equiv> x \<in> set_of X"
 
 lemma in_interval_to_interval[intro!]: "a \<in>\<^sub>i interval_of a"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Interval_Float.thy
--- a/src/HOL/Library/Interval_Float.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Interval_Float.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -92,8 +92,8 @@
   "x \<in>\<^sub>i X" if "lower X \<le> x" "x \<le> upper X"
   using that by (auto simp: set_of_eq)
 
-abbreviation in_real_interval (\<open>(_/ \<in>\<^sub>r _)\<close> [51, 51] 50) where
-  "x \<in>\<^sub>r X \<equiv> x \<in>\<^sub>i real_interval X"
+abbreviation in_real_interval (\<open>(\<open>notation=\<open>infix \<in>\<^sub>r\<close>\<close>_/ \<in>\<^sub>r _)\<close> [51, 51] 50)
+  where "x \<in>\<^sub>r X \<equiv> x \<in>\<^sub>i real_interval X"
 
 lemma in_real_intervalI:
   "x \<in>\<^sub>r X" if "lower X \<le> x" "x \<le> upper X" for x::real and X::"float interval"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -26,39 +26,39 @@
 \<close>
 
 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
-    (\<open>(1O[_]'(_'))\<close>)
+    (\<open>(\<open>indent=1 notation=\<open>mixfix bigo\<close>\<close>O[_]'(_'))\<close>)
   where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
 
 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
-    (\<open>(1o[_]'(_'))\<close>)
+    (\<open>(\<open>indent=1 notation=\<open>mixfix smallo\<close>\<close>o[_]'(_'))\<close>)
   where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
 
 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
-    (\<open>(1\<Omega>[_]'(_'))\<close>)
+    (\<open>(\<open>indent=1 notation=\<open>mixfix bigomega\<close>\<close>\<Omega>[_]'(_'))\<close>)
   where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
 
 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
-    (\<open>(1\<omega>[_]'(_'))\<close>)
+    (\<open>(\<open>indent=1 notation=\<open>mixfix smallomega\<close>\<close>\<omega>[_]'(_'))\<close>)
   where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
 
 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
-    (\<open>(1\<Theta>[_]'(_'))\<close>)
+    (\<open>(\<open>indent=1 notation=\<open>mixfix bigtheta\<close>\<close>\<Theta>[_]'(_'))\<close>)
   where "bigtheta F g = bigo F g \<inter> bigomega F g"
 
-abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where
-  "O(g) \<equiv> bigo at_top g"
+abbreviation bigo_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix bigo\<close>\<close>O'(_'))\<close>)
+  where "O(g) \<equiv> bigo at_top g"
 
-abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where
-  "o(g) \<equiv> smallo at_top g"
+abbreviation smallo_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix smallo\<close>\<close>o'(_'))\<close>)
+  where "o(g) \<equiv> smallo at_top g"
 
-abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where
-  "\<Omega>(g) \<equiv> bigomega at_top g"
+abbreviation bigomega_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix bigomega\<close>\<close>\<Omega>'(_'))\<close>)
+  where "\<Omega>(g) \<equiv> bigomega at_top g"
 
-abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where
-  "\<omega>(g) \<equiv> smallomega at_top g"
+abbreviation smallomega_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix smallomega\<close>\<close>\<omega>'(_'))\<close>)
+  where "\<omega>(g) \<equiv> smallomega at_top g"
 
-abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where
-  "\<Theta>(g) \<equiv> bigtheta at_top g"
+abbreviation bigtheta_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix bigtheta\<close>\<close>\<Theta>'(_'))\<close>)
+  where "\<Theta>(g) \<equiv> bigtheta at_top g"
 
 
 text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>
@@ -1735,7 +1735,7 @@
 named_theorems asymp_equiv_simps
 
 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)
+  (\<open>(\<open>open_block notation=\<open>mixfix asymp_equiv\<close>\<close>_ \<sim>[_] _)\<close> [51, 10, 51] 50)
   where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
 
 abbreviation (input) asymp_equiv_at_top where
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/ListVector.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -99,8 +99,8 @@
 
 subsection "Inner product"
 
-definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" (\<open>\<langle>_,_\<rangle>\<close>) where
-"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
+definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" (\<open>(\<open>open_block notation=\<open>mixfix iprod\<close>\<close>\<langle>_,_\<rangle>)\<close>)
+  where "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
 
 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
 by(simp add: iprod_def)
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -133,22 +133,22 @@
 
 notation
   member_mset  (\<open>'(\<in>#')\<close>) and
-  member_mset  (\<open>(_/ \<in># _)\<close> [50, 51] 50)
+  member_mset  (\<open>(\<open>notation=\<open>infix \<in>#\<close>\<close>_/ \<in># _)\<close> [50, 51] 50)
 
 notation  (ASCII)
   member_mset  (\<open>'(:#')\<close>) and
-  member_mset  (\<open>(_/ :# _)\<close> [50, 51] 50)
+  member_mset  (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<close> [50, 51] 50)
 
 abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
   where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>
 
 notation
   not_member_mset  (\<open>'(\<notin>#')\<close>) and
-  not_member_mset  (\<open>(_/ \<notin># _)\<close> [50, 51] 50)
+  not_member_mset  (\<open>(\<open>notation=\<open>infix \<notin>#\<close>\<close>_/ \<notin># _)\<close> [50, 51] 50)
 
 notation  (ASCII)
   not_member_mset  (\<open>'(~:#')\<close>) and
-  not_member_mset  (\<open>(_/ ~:# _)\<close> [50, 51] 50)
+  not_member_mset  (\<open>(\<open>notation=\<open>infix ~:#\<close>\<close>_/ ~:# _)\<close> [50, 51] 50)
 
 context
 begin
@@ -162,17 +162,18 @@
 end
 
 syntax
-  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<forall>_\<in>#_./ _)\<close> [0, 0, 10] 10)
-  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>_\<in>#_./ _)\<close> [0, 0, 10] 10)
-
+  "_MBall"       :: "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)
+  "_MBex"        :: "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)
 syntax  (ASCII)
-  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
-  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
-
+  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
+  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_MBall" \<rightleftharpoons> Multiset.Ball and
   "_MBex" \<rightleftharpoons> Multiset.Bex
-
 translations
   "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
   "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
@@ -1249,9 +1250,11 @@
 by (rule filter_preserves_multiset)
 
 syntax (ASCII)
-  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    (\<open>(1{#_ :# _./ _#})\<close>)
+  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ :# _./ _#})\<close>)
 syntax
-  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    (\<open>(1{#_ \<in># _./ _#})\<close>)
+  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ \<in># _./ _#})\<close>)
 syntax_consts
   "_MCollect" == filter_mset
 translations
@@ -1824,18 +1827,22 @@
     image_mset_subseteq_mono subset_mset.less_le_not_le)
 
 syntax (ASCII)
-  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  (\<open>({#_/. _ :# _#})\<close>)
+  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+    (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/. _ :# _#})\<close>)
 syntax
-  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  (\<open>({#_/. _ \<in># _#})\<close>)
+  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+    (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/. _ \<in># _#})\<close>)
 syntax_consts
   "_comprehension_mset" \<rightleftharpoons> image_mset
 translations
   "{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
 
 syntax (ASCII)
-  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  (\<open>({#_/ | _ :# _./ _#})\<close>)
+  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+    (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/ | _ :# _./ _#})\<close>)
 syntax
-  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  (\<open>({#_/ | _ \<in># _./ _#})\<close>)
+  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+    (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/ | _ \<in># _./ _#})\<close>)
 syntax_consts
   "_comprehension_mset'" \<rightleftharpoons> image_mset
 translations
@@ -2682,9 +2689,11 @@
 notation sum_mset (\<open>\<Sum>\<^sub>#\<close>)
 
 syntax (ASCII)
-  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  (\<open>(3SUM _:#_. _)\<close> [0, 51, 10] 10)
+  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+    (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _:#_. _)\<close> [0, 51, 10] 10)
 syntax
-  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  (\<open>(3\<Sum>_\<in>#_. _)\<close> [0, 51, 10] 10)
+  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<in>#_. _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_sum_mset_image" \<rightleftharpoons> sum_mset
 translations
@@ -2863,9 +2872,11 @@
 notation prod_mset (\<open>\<Prod>\<^sub>#\<close>)
 
 syntax (ASCII)
-  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  (\<open>(3PROD _:#_. _)\<close> [0, 51, 10] 10)
+  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+    (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _:#_. _)\<close> [0, 51, 10] 10)
 syntax
-  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  (\<open>(3\<Prod>_\<in>#_. _)\<close> [0, 51, 10] 10)
+  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<in>#_. _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_prod_mset_image" \<rightleftharpoons> prod_mset
 translations
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -48,7 +48,7 @@
   where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
 
 definition
-  iter :: "'a list \<Rightarrow> 'a word"  (\<open>(_\<^sup>\<omega>)\<close> [1000])
+  iter :: "'a list \<Rightarrow> 'a word"  (\<open>(\<open>notation=\<open>postfix \<omega>\<close>\<close>_\<^sup>\<omega>)\<close> [1000])
   where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
 
 lemma conc_empty[simp]: "[] \<frown> w = w"
@@ -116,7 +116,8 @@
 definition suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
   where "suffix k x \<equiv> \<lambda>n. x (k+n)"
 
-definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"  (\<open>_ [_ \<rightarrow> _]\<close> 900)
+definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"
+    (\<open>(\<open>open_block notation=\<open>mixfix subsequence\<close>\<close>_ [_ \<rightarrow> _])\<close> 900)
   where "subsequence w i j \<equiv> map w [i..<j]"
 
 abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -17,7 +17,7 @@
   and of_phantom_comp_phantom [simp]: "of_phantom \<circ> phantom = id"
 by(simp_all add: o_def id_def)
 
-syntax "_Phantom" :: "type \<Rightarrow> logic" (\<open>(1Phantom/(1'(_')))\<close>)
+syntax "_Phantom" :: "type \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix Phantom\<close>\<close>Phantom/(1'(_')))\<close>)
 syntax_consts "_Phantom" == phantom
 translations
   "Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Preorder.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -14,7 +14,7 @@
 
 notation
   equiv (\<open>'(\<approx>')\<close>) and
-  equiv (\<open>(_/ \<approx> _)\<close>  [51, 51] 50)
+  equiv (\<open>(\<open>notation=\<open>infix \<approx>\<close>\<close>_/ \<approx> _)\<close>  [51, 51] 50)
 
 lemma equivD1: "x \<le> y" if "x \<approx> y"
   using that by (simp add: equiv_def)
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Quotient_Type.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -76,7 +76,7 @@
 text \<open>Abstracted equivalence classes are the canonical representation of
   elements of a quotient type.\<close>
 
-definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  (\<open>\<lfloor>_\<rfloor>\<close>)
+definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  (\<open>(\<open>open_block notation=\<open>mixfix class\<close>\<close>\<lfloor>_\<rfloor>)\<close>)
   where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
 
 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Ramsey.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -15,7 +15,7 @@
 
 subsubsection \<open>The $n$-element subsets of a set $A$\<close>
 
-definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" (\<open>([_]\<^bsup>_\<^esup>)\<close> [0,999] 999)
+definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" (\<open>(\<open>notation=\<open>mixfix nsets\<close>\<close>[_]\<^bsup>_\<^esup>)\<close> [0,999] 999)
   where "nsets A n \<equiv> {N. N \<subseteq> A \<and> finite N \<and> card N = n}"
 
 lemma finite_imp_finite_nsets: "finite A \<Longrightarrow> finite ([A]\<^bsup>k\<^esup>)"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Real_Mod.thy
--- a/src/HOL/Library/Real_Mod.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Real_Mod.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -106,8 +106,9 @@
 
 
 
-definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" (\<open>(1[_ = _] '(' rmod _'))\<close>) where
-  "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
+definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix rcong\<close>\<close>[_ = _] '(' rmod _'))\<close>)
+  where "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
 
 named_theorems rcong_intros
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Tree.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -9,7 +9,7 @@
 
 datatype 'a tree =
   Leaf (\<open>\<langle>\<rangle>\<close>) |
-  Node "'a tree" ("value": 'a) "'a tree" (\<open>(1\<langle>_,/ _,/ _\<rangle>)\<close>)
+  Node "'a tree" ("value": 'a) "'a tree" (\<open>(\<open>indent=1 notation=\<open>mixfix Node\<close>\<close>\<langle>_,/ _,/ _\<rangle>)\<close>)
 datatype_compat tree
 
 primrec left :: "'a tree \<Rightarrow> 'a tree" where
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Word.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -1685,12 +1685,12 @@
 
 notation
   word_sle    (\<open>'(\<le>s')\<close>) and
-  word_sle    (\<open>(_/ \<le>s _)\<close>  [51, 51] 50) and
+  word_sle    (\<open>(\<open>notation=\<open>infix \<le>s\<close>\<close>_/ \<le>s _)\<close>  [51, 51] 50) and
   word_sless  (\<open>'(<s')\<close>) and
-  word_sless  (\<open>(_/ <s _)\<close>  [51, 51] 50)
+  word_sless  (\<open>(\<open>notation=\<open>infix <s\<close>\<close>_/ <s _)\<close>  [51, 51] 50)
 
 notation (input)
-  word_sle    (\<open>(_/ <=s _)\<close>  [51, 51] 50)
+  word_sle    (\<open>(\<open>notation=\<open>infix <=s\<close>\<close>_/ <=s _)\<close>  [51, 51] 50)
 
 lemma word_sle_eq [code]:
   \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Nonstandard_Analysis/HDeriv.thy
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
 text \<open>Nonstandard Definitions.\<close>
 
 definition nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
-    (\<open>(NSDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+    (\<open>(\<open>notation=\<open>mixfix NSDERIV\<close>\<close>NSDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
   where "NSDERIV f x :> D \<longleftrightarrow>
     (\<forall>h \<in> Infinitesimal - {0}. (( *f* f)(star_of x + h) - star_of (f x)) / h \<approx> star_of D)"
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Nonstandard_Analysis/HLim.thy
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
 text \<open>Nonstandard Definitions.\<close>
 
 definition NSLIM :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
-    (\<open>((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 0, 60] 60)
+    (\<open>(\<open>notation=\<open>mixfix NSLIM\<close>\<close>(_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 0, 60] 60)
   where "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>x. x \<noteq> star_of a \<and> x \<approx> star_of a \<longrightarrow> ( *f* f) x \<approx> star_of L)"
 
 definition isNSCont :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Nonstandard_Analysis/HSEQ.thy
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -16,7 +16,7 @@
 begin
 
 definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
-    (\<open>((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 60] 60) where
+    (\<open>(\<open>notation=\<open>mixfix NSLIMSEQ\<close>\<close>(_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 60] 60) where
     \<comment> \<open>Nonstandard definition of convergence of sequence\<close>
   "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Nonstandard_Analysis/Star.thy
--- a/src/HOL/Nonstandard_Analysis/Star.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/Star.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -11,7 +11,8 @@
 begin
 
 definition  \<comment> \<open>internal sets\<close>
-  starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set"  (\<open>*sn* _\<close> [80] 80)
+  starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set"
+    (\<open>(\<open>open_block notation=\<open>prefix starset_n\<close>\<close>*sn* _)\<close> [80] 80)
   where "*sn* As = Iset (star_n As)"
 
 definition InternalSets :: "'a star set set"
@@ -23,7 +24,8 @@
     (\<forall>x y. \<exists>X \<in> Rep_star x. \<exists>Y \<in> Rep_star y. y = F x \<longleftrightarrow> eventually (\<lambda>n. Y n = f(X n)) \<U>)"
 
 definition  \<comment> \<open>internal functions\<close>
-  starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"  (\<open>*fn* _\<close> [80] 80)
+  starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"
+    (\<open>(\<open>open_block notation=\<open>prefix starfun_n\<close>\<close>*fn* _)\<close> [80] 80)
   where "*fn* F = Ifun (star_n F)"
 
 definition InternalFuns :: "('a star => 'b star) set"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -72,7 +72,8 @@
   by (simp add: FreeUltrafilterNat.proper)
 
 text \<open>Standard principles that play a central role in the transfer tactic.\<close>
-definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" (\<open>(_ \<star>/ _)\<close> [300, 301] 300)
+definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star"
+    (\<open>(\<open>notation=\<open>infix \<star>\<close>\<close>_ \<star>/ _)\<close> [300, 301] 300)
   where "Ifun f \<equiv>
     \<lambda>x. Abs_star (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
 
@@ -183,10 +184,12 @@
 
 text \<open>Nonstandard extensions of functions.\<close>
 
-definition starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"  (\<open>*f* _\<close> [80] 80)
+definition starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"
+    (\<open>(\<open>open_block notation=\<open>prefix starfun\<close>\<close>*f* _)\<close> [80] 80)
   where "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
 
-definition starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> 'c star"  (\<open>*f2* _\<close> [80] 80)
+definition starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> 'c star"
+    (\<open>(\<open>open_block notation=\<open>prefix starfun2\<close>\<close>*f2* _)\<close> [80] 80)
   where "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
 
 declare starfun_def [transfer_unfold]
@@ -270,10 +273,12 @@
 lemma transfer_unstar [transfer_intro]: "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
   by (simp only: unstar_star_n)
 
-definition starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"  (\<open>*p* _\<close> [80] 80)
+definition starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>prefix starP\<close>\<close>*p* _)\<close> [80] 80)
   where "*p* P = (\<lambda>x. unstar (star_of P \<star> x))"
 
-definition starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"  (\<open>*p2* _\<close> [80] 80)
+definition starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>prefix starP2\<close>\<close>*p2* _)\<close> [80] 80)
   where "*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))"
 
 declare starP_def [transfer_unfold]
@@ -332,7 +337,8 @@
 
 text \<open>Nonstandard extensions of sets.\<close>
 
-definition starset :: "'a set \<Rightarrow> 'a star set" (\<open>*s* _\<close> [80] 80)
+definition starset :: "'a set \<Rightarrow> 'a star set"
+    (\<open>(\<open>open_block notation=\<open>prefix starset\<close>\<close>*s* _)\<close> [80] 80)
   where "starset A = Iset (star_of A)"
 
 declare starset_def [transfer_unfold]
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -37,11 +37,13 @@
 context unique_euclidean_semiring
 begin
 
-definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ = _] '(' mod _'))\<close>)
-  where "cong b c a \<longleftrightarrow> b mod a = c mod a"
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix cong\<close>\<close>[_ = _] '(' mod _'))\<close>)
+  where "[b = c] (mod a) \<longleftrightarrow> b mod a = c mod a"
   
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>)
-  where "notcong b c a \<equiv> \<not> cong b c a"
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix notcong\<close>\<close>[_ \<noteq> _] '(' mod _'))\<close>)
+  where "[b \<noteq> c] (mod a) \<equiv> \<not> cong b c a"
 
 lemma cong_refl [simp]:
   "[b = b] (mod a)"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
   stay close to the developments of (finite) products \<^const>\<open>Pi\<^sub>E\<close> and their sigma-algebra
   \<^const>\<open>Pi\<^sub>M\<close>.\<close>
 
-type_notation fmap (\<open>(_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
+type_notation fmap (\<open>(\<open>notation=\<open>infix fmap\<close>\<close>_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
 
 unbundle fmap.lifting
 
@@ -25,7 +25,8 @@
 lemma finite_domain[simp, intro]: "finite (domain P)"
   by transfer simp
 
-lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" (\<open>'((_)')\<^sub>F\<close> [0] 1000) is
+lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix proj\<close>\<close>'(_')\<^sub>F)\<close> [0] 1000) is
   "\<lambda>f x. if x \<in> dom f then the (f x) else undefined" .
 
 declare [[coercion proj]]
@@ -89,7 +90,8 @@
   "Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
 
 syntax
-  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  (\<open>(3\<Pi>'' _\<in>_./ _)\<close>   10)
+  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>'\<close>\<close>\<Pi>'' _\<in>_./ _)\<close>   10)
 syntax_consts
   "_Pi'" == Pi'
 translations
@@ -636,7 +638,8 @@
   "Pi\<^sub>F I M \<equiv> PiF I M"
 
 syntax
-  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  (\<open>(3\<Pi>\<^sub>F _\<in>_./ _)\<close>  10)
+  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>F\<close>\<close>\<Pi>\<^sub>F _\<in>_./ _)\<close>  10)
 syntax_consts
   "_PiF" == PiF
 translations
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Probability/SPMF.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -2621,8 +2621,9 @@
 
 subsection \<open>Try\<close>
 
-definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf" (\<open>TRY _ ELSE _\<close> [0,60] 59)
-where "try_spmf p q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
+definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf"
+  (\<open>(\<open>open_block notation=\<open>mixfix try_spmf\<close>\<close>TRY _ ELSE _)\<close> [0,60] 59)
+where "TRY p ELSE q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
 
 lemma try_spmf_lossless [simp]:
   assumes "lossless_spmf p"
diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Unix/Unix.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -336,7 +336,7 @@
 \<close>
 
 inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
-  (\<open>_ \<midarrow>_\<rightarrow> _\<close> [90, 1000, 90] 100)
+  (\<open>(\<open>open_block notation=\<open>mixfix transition\<close>\<close>_ \<midarrow>_\<rightarrow> _)\<close> [90, 1000, 90] 100)
   where
     read:
       "root \<midarrow>(Read uid text path)\<rightarrow> root"
@@ -475,7 +475,8 @@
   running processes over a finite amount of time.
 \<close>
 
-inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"  (\<open>_ \<Midarrow>_\<Rightarrow> _\<close> [90, 1000, 90] 100)
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
+    (\<open>(\<open>open_block notation=\<open>mixfix transitions\<close>\<close>_ \<Midarrow>_\<Rightarrow> _)\<close> [90, 1000, 90] 100)
   where
     nil: "root \<Midarrow>[]\<Rightarrow> root"
   | cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"