diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -194,6 +194,9 @@
   unfolding differentiable_def
   by auto
 
+lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
+  using differentiable_on_def by blast
+
 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
   unfolding differentiable_def
   using has_derivative_at_within