diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Multivariate_Analysis/Derivative.thy
--- 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