--- 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"