src/HOL/Computational_Algebra/Formal_Power_Series.thy
 changeset 66804 3f9bb52082c4 parent 66550 e5d82cf3c387 child 66806 a4e82b58d833
```     1.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:20 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:20 2017 +0200
1.3 @@ -3133,7 +3133,7 @@
1.4        done
1.5      also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a\$(i+1) * (sum (\<lambda>j. (b^ i)\$j * of_nat (n - j + 1) * b\$(n - j + 1)) {0..n})) {0.. n}"
1.6        unfolding sum_distrib_left
1.7 -      apply (subst sum.commute)
1.8 +      apply (subst sum.swap)
1.9        apply (rule sum.cong, rule refl)+
1.10        apply simp
1.11        done
1.12 @@ -3314,7 +3314,7 @@
1.13      done
1.14    have "?r =  sum (\<lambda>i. sum (\<lambda>(k,m). a\$k * (c^k)\$i * b\$m * (d^m) \$ (n - i)) {(k,m). k + m \<le> n}) {0..n}"
1.15      apply (simp add: fps_mult_nth sum_distrib_left)
1.16 -    apply (subst sum.commute)
1.17 +    apply (subst sum.swap)
1.18      apply (rule sum.cong)
1.19      apply (auto simp add: field_simps)
1.20      done
```