src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 66793 deabce3ccf1f
parent 66709 b034d2ae541c
child 66884 c2128ab11f61
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -6467,7 +6467,7 @@
     1.4    qed
     1.5    have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
     1.6                    (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
     1.7 -    using deriv[of x] that by (simp add: at_within_closed_interval o_def)
     1.8 +    using deriv[of x] that by (simp add: at_within_Icc_at o_def)
     1.9    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
    1.10      using le cont_int s deriv cont_int
    1.11      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all