# HG changeset patch # User paulson # Date 1754470865 -3600 # Node ID cbf3703f92ea409c2ff138c08ce18fb51397b0aa # Parent 7c870287f04f984f9455febcf1e0a4258c7bb191 fixed a markup issue diff -r 7c870287f04f -r cbf3703f92ea src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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 \Definite integrals for exponential and power function\ -text \This lemma packages up a reference to @{thm[source]monotone_convergence_increasing}}\ +text \This lemma packages up a reference to @{thm[source]monotone_convergence_increasing}\ lemma has_integral_to_inf: fixes h ::"real \ real" assumes int: "\y::real. h integrable_on {a..y}"