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