src/HOL/NthRoot.thy
changeset 64267 b9a1486e79be
parent 64122 74fde524799e
child 65552 f533820e7248
     1.1 --- a/src/HOL/NthRoot.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -720,7 +720,7 @@
     1.4          by (simp add: x_def)
     1.5        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
     1.6          using \<open>2 < n\<close>
     1.7 -        by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
     1.8 +        by (intro sum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
     1.9        also have "\<dots> = (x n + 1) ^ n"
    1.10          by (simp add: binomial_ring)
    1.11        also have "\<dots> = n"
    1.12 @@ -761,7 +761,7 @@
    1.13            by (simp add: x_def)
    1.14          also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    1.15            using \<open>1 < n\<close> \<open>1 \<le> c\<close>
    1.16 -          by (intro setsum_mono2)
    1.17 +          by (intro sum_mono2)
    1.18              (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    1.19          also have "\<dots> = (x n + 1) ^ n"
    1.20            by (simp add: binomial_ring)