changeset 62348 | 9a5f43dac883 |
parent 61933 | cf58b5b794b2 |
child 63680 | 6e1e8b5abbfa |
--- a/src/HOL/ex/NatSum.thy Wed Feb 17 21:51:57 2016 +0100 +++ b/src/HOL/ex/NatSum.thy Wed Feb 17 21:51:57 2016 +0100 @@ -98,7 +98,7 @@ "30 * int (\<Sum>i=0..<m. i * i * i * i) = int m * (int m - 1) * (int(2 * m) - 1) * (int(3 * m * m) - int(3 * m) - 1)" - by (induct m) (simp_all add: int_mult) + by (induct m) (simp_all add: of_nat_mult) lemma of_nat_sum_of_fourth_powers: "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =