changeset 57418 | 6ab1c7cb0b8d |
parent 56788 | 28ff163eefef |
child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/ex/HarmonicSeries.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/ex/HarmonicSeries.thy Sat Jun 28 09:16:42 2014 +0200 @@ -196,7 +196,7 @@ "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}" by auto ultimately show ?thesis - by (auto intro: setsum_Un_disjoint) + by (auto intro: setsum.union_disjoint) qed moreover {