lemma lemma_DERIV_subst moved to Deriv.thy

--- a/src/HOL/Hyperreal/Deriv.thy	Tue Jun 05 16:26:07 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Tue Jun 05 16:31:10 2007 +0200
@@ -1384,4 +1384,7 @@
   with g'cdef f'cdef cint show ?thesis by auto
 qed
 
+lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
+by auto
+
 end

--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 16:26:07 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 16:31:10 2007 +0200
@@ -987,9 +987,6 @@
 apply (rule isCont_inverse_function [where f=exp], simp_all)
 done
 
-lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by simp (* TODO: put in Deriv.thy *)
-
 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
 apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
 apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])