--- a/src/HOL/Deriv.thy Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Deriv.thy Wed Jul 13 17:14:17 2016 +0100
@@ -82,6 +82,9 @@
lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
by (simp add: has_derivative_def)
+lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)"
+ by (metis eq_id_iff has_derivative_ident)
+
lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
by (simp add: has_derivative_def)