diff -r bc0fc5499085 -r f0c894ab18c9 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 21 19:08:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 22 14:33:34 2015 +0000
@@ -2356,6 +2356,10 @@
 lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
   unfolding deriv_def by (metis some_equality DERIV_unique)
 
+lemma DERIV_deriv_iff_has_field_derivative:
+  "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
+  by (auto simp: has_field_derivative_def DERIV_imp_deriv)
+  
 lemma DERIV_deriv_iff_real_differentiable:
   fixes x :: real
   shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"