--- a/src/HOL/Probability/Caratheodory.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Mar 18 22:11:46 2014 +0100
@@ -40,9 +40,9 @@
by (auto intro!: setsum_mono3 simp: pos) }
ultimately
show ?thesis unfolding g_def using pos
- by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex SUP_upper2
- setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair
- SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
+ by (auto intro!: SUP_eq simp: setsum_cartesian_product reindex SUP_upper2
+ setsum_nonneg suminf_ereal_eq_SUP SUP_pair
+ SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
qed
subsection {* Measure Spaces *}