src/HOL/Transcendental.thy
changeset 44317 b7e9fa025f15
parent 44316 84b6f7a6cea4
child 44318 425c1f8f9487
     1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 17:59:19 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 18:06:27 2011 -0700
     1.3 @@ -1166,7 +1166,7 @@
     1.4  
     1.5  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
     1.6    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
     1.7 -  apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
     1.8 +  apply (erule DERIV_cong [OF DERIV_exp exp_ln])
     1.9    apply (simp_all add: abs_if isCont_ln)
    1.10    done
    1.11  
    1.12 @@ -1309,9 +1309,6 @@
    1.13  lemma cos_zero [simp]: "cos 0 = 1"
    1.14    unfolding cos_def cos_coeff_def by (simp add: powser_zero)
    1.15  
    1.16 -lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    1.17 -  by (rule DERIV_cong) (* TODO: delete *)
    1.18 -
    1.19  lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
    1.20  proof -
    1.21    have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"