--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 24 14:22:29 2014 +0000
@@ -289,20 +289,6 @@
unfolding differentiable_on_def continuous_on_eq_continuous_within
using differentiable_imp_continuous_within by blast
-lemma has_derivative_within_subset:
- "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
- (f has_derivative f') (at x within t)"
- unfolding has_derivative_within
- using tendsto_within_subset
- by blast
-
-lemma differentiable_within_subset:
- "f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow>
- f differentiable (at x within s)"
- unfolding differentiable_def
- using has_derivative_within_subset
- by blast
-
lemma differentiable_on_subset:
"f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
unfolding differentiable_on_def