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