--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Feb 19 11:58:51 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 21 15:04:01 2017 +0000
@@ -1386,7 +1386,7 @@
else Ln(z) - \<i> * of_real(3 * pi/2))"
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
- by (auto simp: Ln_times)
+ by (simp add: Ln_times) auto
lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all