src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 69510 0f31dd2e540d
parent 69508 2a4c8a2a3f8e
child 69517 dc20f278e8f3
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 19:48:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 21:00:50 2018 +0100
     1.3 @@ -5924,7 +5924,7 @@
     1.4        next
     1.5          have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
     1.6                \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
     1.7 -          apply (subst sum_group)
     1.8 +          apply (subst sum.group)
     1.9            using s by (auto simp: sum_subtractf split_def p'(1))
    1.10          also have "\<dots> < e/2"
    1.11          proof -