src/HOL/Inequalities.thy
changeset 61762 d50b993b4fb9
parent 61694 6571c78c9667
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Inequalities.thy	Mon Nov 30 14:24:51 2015 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Tue Dec 01 14:09:10 2015 +0000
     1.3 @@ -66,7 +66,6 @@
     1.4        using assms by (cases "i \<le> j") (auto simp: algebra_simps)
     1.5    } hence "?S \<le> 0"
     1.6      by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
     1.7 -       (auto simp: field_simps)
     1.8    finally show ?thesis by (simp add: algebra_simps)
     1.9  qed
    1.10