diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -886,11 +886,11 @@
 
 end
 
-definition\<^marker>\<open>tag important\<close> lebesgue_integral ("integral\<^sup>L") where
+definition\<^marker>\<open>tag important\<close> lebesgue_integral (\<open>integral\<^sup>L\<close>) where
   "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" ("\<integral>((2 _./ _)/ \<partial>_)" [60,61] 110)
+  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" (\<open>\<integral>((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
 
 syntax_consts
   "_lebesgue_integral" == lebesgue_integral
@@ -899,7 +899,7 @@
   "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
 
 syntax
-  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
+  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" (\<open>(3LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
 
 syntax_consts
   "_ascii_lebesgue_integral" == lebesgue_integral