# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1504035283 -3600
# Node ID 19bf4d5966dce39d88ff958d000a1ae2cfafc625
# Parent  6ab32ffb2bddb385c02c53765e18f239b2236ac1
correction to my previous commit

diff -r 6ab32ffb2bdd -r 19bf4d5966dc src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Tue Aug 29 17:41:27 2017 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Tue Aug 29 20:34:43 2017 +0100
@@ -261,8 +261,8 @@
   have f'_nonpos: "f' \<le> 0" using assms by (simp add: f'_def divide_simps)
   let ?f = "\<lambda>t. (t - x) * f' + inverse x"
   let ?F = "\<lambda>t. (t - x)^2 * f' / 2 + t * inverse x"
-  have diff: "\<forall>t\<in>{x..x+a}. (?F has_vector_derivative ?f t)
-                               (at t within {x..x+a})" using assms
+  have diff: "\<And>t. t \<in> {x..x+a} \<Longrightarrow> (?F has_vector_derivative ?f t) (at t within {x..x+a})" 
+    using assms
     by (auto intro!: derivative_eq_intros
              simp: has_field_derivative_iff_has_vector_derivative[symmetric])
   from assms have "(?f has_integral (?F (x+a) - ?F x)) {x..x+a}"