# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1526843670 -3600
# Node ID fa63bde6d65965e0a2de651b7f7a7e53850d0c76
# Parent  0764ee22a4d19baa90a7d892da38385b197ef34b
one last fix

diff -r 0764ee22a4d1 -r fa63bde6d659 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Sun May 20 18:37:34 2018 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy	Sun May 20 20:14:30 2018 +0100
@@ -814,7 +814,7 @@
     note s
     also note \<open>cball t v \<subseteq> T\<close>
     finally
-    have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
+    have deriv: "\<And>y. y \<in> cball x u \<Longrightarrow> (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
       using \<open>_ \<subseteq> X\<close>
       by (auto intro!: has_derivative_at_withinI[OF f'])
     have "norm (f s y - f s z) \<le> B * norm (y - z)"