--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 20 19:51:08 2024 +0200
@@ -964,7 +964,7 @@
abbreviation
absolutely_integrable_on :: "('a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
- (infixr "absolutely'_integrable'_on" 46)
+ (infixr \<open>absolutely'_integrable'_on\<close> 46)
where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"