removed junk;
authorwenzelm
Thu, 04 Mar 2021 22:46:44 +0100
changeset 73620 3bb9df8900fd
parent 73619 10b9b3341c26
child 73621 99fbb7c7de22
child 73625 39826af584bf
removed junk;
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)"