src/HOL/Deriv.thy

 
 corollary DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
   by (rule DERIV_continuous)
 
 lemma DERIV_continuous_on:
-  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x)) \<Longrightarrow> continuous_on s f"
-  by (metis DERIV_continuous continuous_at_imp_continuous_on)
+  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x within s)) \<Longrightarrow> continuous_on s f"
+  unfolding continuous_on_eq_continuous_within
+  by (intro continuous_at_imp_continuous_on ballI DERIV_continuous) 
 
 lemma DERIV_mult':
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])