--- a/src/HOL/Deriv.thy Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Deriv.thy Wed Apr 02 18:35:01 2014 +0200
@@ -61,6 +61,9 @@
lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
by (simp add: has_derivative_def)
+lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
+ using bounded_linear.linear[OF has_derivative_bounded_linear] .
+
lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
by (simp add: has_derivative_def tendsto_const)