--- a/src/HOL/Probability/Projective_Limit.thy Tue Jul 28 13:00:54 2015 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Jul 28 16:16:13 2015 +0100
@@ -350,9 +350,8 @@
by (simp add: setsum_left_distrib)
also have "\<dots> < ereal (1 * real ?a)" unfolding less_ereal.simps
proof (rule mult_strict_right_mono)
- have "(\<Sum>i\<in>{1..n}. 2 powr - real i) = (\<Sum>i\<in>{1..<Suc n}. (1/2) ^ i)"
- by (rule setsum.cong)
- (auto simp: powr_realpow[symmetric] powr_minus powr_divide inverse_eq_divide)
+ have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)"
+ by (rule setsum.cong) (auto simp: powr_realpow powr_divide powr_minus_divide)
also have "{1..<Suc n} = {..<Suc n} - {0}" by auto
also have "setsum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) =
setsum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: setsum_diff1)