correction to my previous commit
authorpaulson <lp15@cam.ac.uk>
Tue, 29 Aug 2017 20:34:43 +0100
changeset 66554 19bf4d5966dc
parent 66553 6ab32ffb2bdd
child 66555 87b9eb69d5ba
child 66557 116f658195af
child 66559 39257f39c7da
correction to my previous commit
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}"