src/HOL/Transcendental.thy
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