--- 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