changeset 52141 eff000cab70f
parent 51329 4a3c453f99a1
child 55642 63beb38e9258
--- a/src/HOL/Probability/Caratheodory.thy	Sat May 25 15:44:08 2013 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Sat May 25 15:44:29 2013 +0200
@@ -707,9 +707,9 @@
   assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
   shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
 proof -
-  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>A`I \<in> M"
+  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
     using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
-  with `volume M f` have "f (\<Union>A`I) = (\<Sum>a\<in>A`I. f a)"
+  with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
     unfolding volume_def by blast
   also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
   proof (subst setsum_reindex_nonzero)