changeset 61694 | 6571c78c9667 |
parent 61649 | 268d88ec9087 |
child 61762 | d50b993b4fb9 |
--- a/src/HOL/Inequalities.thy Tue Nov 17 12:01:19 2015 +0100 +++ b/src/HOL/Inequalities.thy Tue Nov 17 12:32:08 2015 +0000 @@ -34,7 +34,7 @@ by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum split: zdiff_int_split) thus ?thesis - using int_int_eq by blast + using of_nat_eq_iff by blast qed lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"