src/HOL/Probability/Caratheodory.thy
changeset 56212 3253aaf73a01
parent 56166 9a241bc276cd
child 56994 8d5e5ec1cac3
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -40,9 +40,9 @@
     1.4        by (auto intro!: setsum_mono3 simp: pos) }
     1.5    ultimately
     1.6    show ?thesis unfolding g_def using pos
     1.7 -    by (auto intro!: SUPR_eq  simp: setsum_cartesian_product reindex SUP_upper2
     1.8 -                     setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair
     1.9 -                     SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    1.10 +    by (auto intro!: SUP_eq  simp: setsum_cartesian_product reindex SUP_upper2
    1.11 +                     setsum_nonneg suminf_ereal_eq_SUP SUP_pair
    1.12 +                     SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    1.13  qed
    1.14  
    1.15  subsection {* Measure Spaces *}