src/HOL/Analysis/Complex_Transcendental.thy
changeset 65578 e4997c181cce
parent 65274 db2de50de28e
child 65583 8d53b3bebab4
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -709,6 +709,7 @@
     1.4    apply (simp only: pos_le_divide_eq [symmetric], linarith)
     1.5    done
     1.6  
     1.7 +text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
     1.8  lemma e_less_3: "exp 1 < (3::real)"
     1.9    using e_approx_32
    1.10    by (simp add: abs_if split: if_split_asm)
    1.11 @@ -1752,7 +1753,7 @@
    1.12  declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
    1.13  
    1.14  
    1.15 -lemma has_field_derivative_powr_right:
    1.16 +lemma has_field_derivative_powr_right [derivative_intros]:
    1.17      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
    1.18    apply (simp add: powr_def)
    1.19    apply (intro derivative_eq_intros | simp)+