src/HOL/Computational_Algebra/Formal_Power_Series.thy
changeset 65578 e4997c181cce
parent 65435 378175f44328
child 66089 def95e0bc529
     1.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -913,7 +913,7 @@
     1.4    then have "exp (real k * ln y + ln x) > exp 0"
     1.5      by (simp add: ac_simps)
     1.6    then have "y ^ k * x > 1"
     1.7 -    unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
     1.8 +    unfolding exp_zero exp_add exp_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
     1.9      by simp
    1.10    then have "x > (1 / y)^k" using yp
    1.11      by (simp add: field_simps)