--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 03 20:34:24 2025 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 06 10:01:05 2025 +0100
@@ -7299,7 +7299,7 @@
subsection \<open>Definite integrals for exponential and power function\<close>
-text \<open>This lemma packages up a reference to @{thm[source]monotone_convergence_increasing}}\<close>
+text \<open>This lemma packages up a reference to @{thm[source]monotone_convergence_increasing}\<close>
lemma has_integral_to_inf:
fixes h ::"real \<Rightarrow> real"
assumes int: "\<And>y::real. h integrable_on {a..y}"