# HG changeset patch
# User wenzelm
# Date 1727858144 -7200
# Node ID 6c81cdca5b82585acebafea3dca531342e196c8b
# Parent  e957b2dd8983defdb58b6ed6d10127a79fb61194
more inner syntax markup: HOL-Analysis;

diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -890,7 +890,8 @@
   "integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
 
 syntax
-  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" (\<open>\<integral>((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real"
+    (\<open>(\<open>indent=1 notation=\<open>binder integral\<close>\<close>\<integral>(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
 
 syntax_consts
   "_lebesgue_integral" == lebesgue_integral
@@ -899,7 +900,8 @@
   "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
 
 syntax
-  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" (\<open>(3LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
+  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+    (\<open>(\<open>indent=3 notation=\<open>mixfix LINT\<close>\<close>LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
 
 syntax_consts
   "_ascii_lebesgue_integral" == lebesgue_integral
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -10,7 +10,7 @@
 
 definition\<^marker>\<open>tag important\<close> "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
 
-typedef (overloaded) ('a, 'b) bcontfun (\<open>(_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
+typedef (overloaded) ('a, 'b) bcontfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>C\<close>\<close>_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
   "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
   morphisms apply_bcontfun Bcontfun
   by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -116,7 +116,7 @@
 
 subsection \<open>Type of bounded linear functions\<close>
 
-typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
+typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>L\<close>\<close>_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
   "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
   morphisms blinfun_apply Blinfun
   by (blast intro: bounded_linear_intros)
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -169,7 +169,8 @@
   "Pi\<^sub>M I M \<equiv> PiM I M"
 
 syntax
-  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  (\<open>(3\<Pi>\<^sub>M _\<in>_./ _)\<close>  10)
+  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>M\<close>\<close>\<Pi>\<^sub>M _\<in>_./ _)\<close>  10)
 syntax_consts
   "_PiM" == PiM
 translations
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -96,10 +96,10 @@
 
 syntax (ASCII)
   "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
 syntax
   "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(2\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_infsetsum" \<rightleftharpoons> infsetsum
 translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -107,10 +107,10 @@
 
 syntax (ASCII)
   "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
 syntax
   "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
-  (\<open>(2\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
 syntax_consts
   "_uinfsetsum" \<rightleftharpoons> infsetsum
 translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -118,10 +118,10 @@
 
 syntax (ASCII)
   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
-  (\<open>(3INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
 syntax
   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
-  (\<open>(2\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qinfsetsum" \<rightleftharpoons> infsetsum
 translations
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -47,27 +47,29 @@
   "f abs_summable_on A \<equiv> (\<lambda>x. norm (f x)) summable_on A"
 
 syntax (ASCII)
-  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"  (\<open>(3INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
+  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+    (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
 syntax
-  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"  (\<open>(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+    (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
 syntax_consts
   "_infsum" \<rightleftharpoons> infsum
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
 
 syntax (ASCII)
-  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3INFSUM _./ _)\<close> [0, 10] 10)
+  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _./ _)\<close> [0, 10] 10)
 syntax
-  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(2\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
+  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
 syntax_consts
   "_univinfsum" \<rightleftharpoons> infsum
 translations
   "\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
 
 syntax (ASCII)
-  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
 syntax
-  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
+  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qinfsum" \<rightleftharpoons> infsum
 translations
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -391,9 +391,8 @@
 subsection \<open>Gradient derivative\<close>
 
 definition\<^marker>\<open>tag important\<close>
-  gderiv ::
-    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
-          (\<open>(GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+  gderiv :: "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
+    (\<open>(\<open>notation=\<open>mixfix GDERIV\<close>\<close>GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
 where
   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
 
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -146,7 +146,7 @@
 
 syntax
   "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(5LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
+  (\<open>(\<open>indent=5 notation=\<open>binder LINT\<close>\<close>LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
 
 syntax_consts
   "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
@@ -160,7 +160,7 @@
 
 syntax
   "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(4LBINT _=_.._. _)\<close> [0,60,60,61] 60)
+  (\<open>(\<open>indent=4 notation=\<open>binder LBINT\<close>\<close>LBINT _=_.._. _)\<close> [0,60,60,61] 60)
 
 syntax_consts
   "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
@@ -1049,7 +1049,7 @@
 
 
 syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
-  (\<open>(2CLBINT _. _)\<close> [0,60] 60)
+  (\<open>(\<open>indent=2 notation=\<open>binder CLBINT\<close>\<close>CLBINT _. _)\<close> [0,60] 60)
 
 syntax_consts
   "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
@@ -1057,7 +1057,7 @@
 translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
 
 syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
-  (\<open>(3CLBINT _:_. _)\<close> [0,60,61] 60)
+  (\<open>(\<open>indent=3 notation=\<open>binder CLBINT\<close>\<close>CLBINT _:_. _)\<close> [0,60,61] 60)
 
 syntax_consts
   "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
@@ -1075,7 +1075,7 @@
 
 syntax
   "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
-  (\<open>(4CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
+  (\<open>(\<open>indent=4 notation=\<open>binder CLBINT\<close>\<close>CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
 
 syntax_consts
   "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -820,7 +820,7 @@
   "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
 
 syntax
-  "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>\<integral>\<^sup>+((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+  "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>(\<open>indent=2 notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
 
 syntax_consts
   "_nn_integral" == nn_integral
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -24,7 +24,7 @@
 
 syntax
   "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(4LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
+  (\<open>(\<open>indent=4 notation=\<open>binder LINT\<close>\<close>LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
 
 syntax_consts
   "_ascii_set_lebesgue_integral" == set_lebesgue_integral
@@ -43,11 +43,11 @@
 
 syntax
   "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(2LBINT _./ _)\<close> [0,10] 10)
+  (\<open>(\<open>indent=2 notation=\<open>binder LBINT\<close>\<close>LBINT _./ _)\<close> [0,10] 10)
 
 syntax
   "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(3LBINT _:_./ _)\<close> [0,0,10] 10)
+  (\<open>(\<open>indent=3 notation=\<open>binder LBINT\<close>\<close>LBINT _:_./ _)\<close> [0,0,10] 10)
 
 section \<open>Basic properties\<close>
 
@@ -587,7 +587,7 @@
 
 syntax
   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(3CLINT _|_. _)\<close> [0,0,10] 10)
+  (\<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
@@ -624,7 +624,7 @@
 
 syntax
   "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  (\<open>(4CLINT _:_|_. _)\<close> [0,0,0,10] 10)
+  (\<open>(\<open>indent=4 notation=\<open>binder CLINT\<close>\<close>CLINT _:_|_. _)\<close> [0,0,0,10] 10)
 
 syntax_consts
   "_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
@@ -647,10 +647,10 @@
 
 syntax
 "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<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>(\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<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
diff -r e957b2dd8983 -r 6c81cdca5b82 src/HOL/Analysis/Sparse_In.thy
--- a/src/HOL/Analysis/Sparse_In.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -165,14 +165,14 @@
  "cosparse A = Abs_filter (\<lambda>P. {x. \<not>P x} sparse_in A)"
 
 syntax
-  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  (\<open>(3\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
+  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_eventually_cosparse" == eventually
 translations
   "\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
 
 syntax
-  "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(3\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
+  "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
 syntax_consts
   "_qeventually_cosparse" == eventually
 translations