# HG changeset patch
# User wenzelm
# Date 1614894404 -3600
# Node ID 3bb9df8900fdc56439616fb134b4e3e2817f2f48
# Parent  10b9b3341c26aebfe71cbd4e18cdabe3b796ff57
removed junk;

diff -r 10b9b3341c26 -r 3bb9df8900fd src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Mar 04 22:44:31 2021 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Mar 04 22:46:44 2021 +0100
@@ -3729,7 +3729,6 @@
     then have eba8: "(e * (b-a)) / 8 > 0"
       using ab by (auto simp add: field_simps)
     note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt, THEN conjunct2, rule_format]
-    thm derf_exp
     have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
       by (simp add: bounded_linear_scaleR_left)
     have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"