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