src/HOL/Analysis/Caratheodory.thy
changeset 66804 3f9bb52082c4
parent 65680 378a2f11bec9
child 67682 00c436488398
     1.1 --- a/src/HOL/Analysis/Caratheodory.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4    qed
     1.5    also have "\<dots> = (SUP p. \<Sum>i<p. \<Sum>n. f (i, n))"
     1.6      unfolding suminf_sum[OF summableI, symmetric]
     1.7 -    by (simp add: suminf_eq_SUP SUP_pair sum.commute[of _ "{..< fst _}"])
     1.8 +    by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"])
     1.9    finally show ?thesis unfolding g_def
    1.10      by (simp add: suminf_eq_SUP)
    1.11  qed
    1.12 @@ -592,7 +592,7 @@
    1.13      assume "\<Union>C = \<Union>D"
    1.14      with split_sum[OF C D] split_sum[OF D C]
    1.15      have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
    1.16 -      by (simp, subst sum.commute, simp add: ac_simps) }
    1.17 +      by (simp, subst sum.swap, simp add: ac_simps) }
    1.18    note sum_eq = this
    1.19  
    1.20    { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"