src/HOL/Probability/Caratheodory.thy
changeset 56166 9a241bc276cd
parent 55642 63beb38e9258
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -975,7 +975,7 @@
     1.4      have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
     1.5        using C' A'
     1.6        by (subst volume_finite_additive[symmetric, OF V(1)])
     1.7 -         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq
     1.8 +         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
     1.9                 intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
    1.10                 intro: generated_ringI_Basic)
    1.11      also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
    1.12 @@ -987,7 +987,7 @@
    1.13      also have "\<dots> = \<mu>_r (\<Union>C')"
    1.14        using C' Un_A
    1.15        by (subst volume_finite_additive[symmetric, OF V(1)])
    1.16 -         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq 
    1.17 +         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq 
    1.18                 intro: generated_ringI_Basic)
    1.19      finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
    1.20        using C' by simp