--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jul 27 16:52:57 2015 +0100
@@ -2315,4 +2315,9 @@
lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
by (simp add: vector_derivative_at)
+lemma vector_derivative_at_within_ivl:
+ "(f has_vector_derivative f') (at x) \<Longrightarrow>
+ a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
+using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+
end