lemma lemma_DERIV_subst moved to Deriv.thy
authorchaieb
Tue Jun 05 16:31:10 2007 +0200 (2007-06-05)
changeset 23255631bd424fd72
parent 23254 99644a53f16d
child 23256 d797768d5655
lemma lemma_DERIV_subst moved to Deriv.thy
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/Deriv.thy	Tue Jun 05 16:26:07 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Tue Jun 05 16:31:10 2007 +0200
     1.3 @@ -1384,4 +1384,7 @@
     1.4    with g'cdef f'cdef cint show ?thesis by auto
     1.5  qed
     1.6  
     1.7 +lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
     1.8 +by auto
     1.9 +
    1.10  end
     2.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 16:26:07 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 16:31:10 2007 +0200
     2.3 @@ -987,9 +987,6 @@
     2.4  apply (rule isCont_inverse_function [where f=exp], simp_all)
     2.5  done
     2.6  
     2.7 -lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
     2.8 -by simp (* TODO: put in Deriv.thy *)
     2.9 -
    2.10  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
    2.11  apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
    2.12  apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])