src/HOL/Series.thy
changeset 59741 5b762cd73a8e
parent 59712 6c013328b885
child 60141 833adf7db7d8
     1.1 --- a/src/HOL/Series.thy	Tue Mar 17 17:45:03 2015 +0000
     1.2 +++ b/src/HOL/Series.thy	Wed Mar 18 14:13:27 2015 +0000
     1.3 @@ -434,7 +434,7 @@
     1.4    have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
     1.5      by auto
     1.6    have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
     1.7 -    by simp
     1.8 +    by (simp add: mult.commute)
     1.9    thus ?thesis using sums_divide [OF 2, of 2]
    1.10      by simp
    1.11  qed