--- a/src/HOL/Inequalities.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Inequalities.thy Fri May 27 20:23:55 2016 +0200
@@ -58,8 +58,8 @@
proof -
let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
have "2 * (of_nat n * (\<Sum>j=0..<n. (a j * b j)) - (\<Sum>j=0..<n. b j) * (\<Sum>k=0..<n. a k)) = ?S"
- unfolding one_add_one[symmetric] algebra_simps
- by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
+ by (simp only: one_add_one[symmetric] algebra_simps)
+ (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
also
{ fix i j::nat assume "i<n" "j<n"
hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0"