correction to my previous commit
authorpaulson <lp15@cam.ac.uk>
Tue Aug 29 20:34:43 2017 +0100 (2017-08-29)
changeset 6655419bf4d5966dc
parent 66553 6ab32ffb2bdd
child 66555 39257f39c7da
child 66560 116f658195af
child 66563 87b9eb69d5ba
correction to my previous commit
src/HOL/Analysis/Harmonic_Numbers.thy
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Tue Aug 29 17:41:27 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Tue Aug 29 20:34:43 2017 +0100
     1.3 @@ -261,8 +261,8 @@
     1.4    have f'_nonpos: "f' \<le> 0" using assms by (simp add: f'_def divide_simps)
     1.5    let ?f = "\<lambda>t. (t - x) * f' + inverse x"
     1.6    let ?F = "\<lambda>t. (t - x)^2 * f' / 2 + t * inverse x"
     1.7 -  have diff: "\<forall>t\<in>{x..x+a}. (?F has_vector_derivative ?f t)
     1.8 -                               (at t within {x..x+a})" using assms
     1.9 +  have diff: "\<And>t. t \<in> {x..x+a} \<Longrightarrow> (?F has_vector_derivative ?f t) (at t within {x..x+a})" 
    1.10 +    using assms
    1.11      by (auto intro!: derivative_eq_intros
    1.12               simp: has_field_derivative_iff_has_vector_derivative[symmetric])
    1.13    from assms have "(?f has_integral (?F (x+a) - ?F x)) {x..x+a}"