src/HOL/Transcendental.thy
changeset 47489 04e7d09ade7a
parent 47108 2a1953f0d20d
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Transcendental.thy	Sun Apr 15 20:51:07 2012 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Apr 16 11:24:57 2012 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4           order_trans [OF norm_setsum]
     1.5           real_setsum_nat_ivl_bounded2
     1.6           mult_nonneg_nonneg
     1.7 -         zero_le_imp_of_nat
     1.8 +         of_nat_0_le_iff
     1.9           zero_le_power K)
    1.10        apply (rule le_Kn, simp)
    1.11        done