src/HOL/Analysis/Complex_Transcendental.thy
changeset 65036 ab7e11730ad8
parent 64790 ed38f9a834d8
child 65064 a4abec71279a
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Feb 19 11:58:51 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 21 15:04:01 2017 +0000
     1.3 @@ -1386,7 +1386,7 @@
     1.4                            else Ln(z) - \<i> * of_real(3 * pi/2))"
     1.5    using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
     1.6          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
     1.7 -  by (auto simp: Ln_times)
     1.8 +  by (simp add: Ln_times) auto 
     1.9  
    1.10  lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
    1.11    by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all