src/HOL/Analysis/Lipschitz.thy

   have lipschitz: "B-lipschitz_on (cball x (min u v) \<inter> X) (f s)" if s: "s \<in> cball t v" for s
   proof -
     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)"
       if "y \<in> cball x u" "z \<in> cball x u"
       for y z