changeset 49784 | 5e5b2da42a69 |
parent 49780 | 92a58f80b20c |
child 49999 | dfb63b9b8908 |
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 @@ -751,7 +751,6 @@ show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F using fin by (auto simp: prod_algebra_eq_finite) - show "incseq ?F" by fact show "(\<Union>i. \<Pi>\<^isub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i))" using F(3) by (simp add: space_PiM) next