--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Apr 25 16:39:54 2017 +0100
@@ -709,6 +709,7 @@
apply (simp only: pos_le_divide_eq [symmetric], linarith)
done
+text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
lemma e_less_3: "exp 1 < (3::real)"
using e_approx_32
by (simp add: abs_if split: if_split_asm)
@@ -1752,7 +1753,7 @@
declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
-lemma has_field_derivative_powr_right:
+lemma has_field_derivative_powr_right [derivative_intros]:
"w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
apply (simp add: powr_def)
apply (intro derivative_eq_intros | simp)+