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