changeset 69313 | b021008c5397 |
parent 69219 | d4cec24a1d87 |
child 69655 | 2b56cbb02e8a |
--- a/src/HOL/Probability/Tree_Space.thy Sun Nov 18 09:51:41 2018 +0100 +++ b/src/HOL/Probability/Tree_Space.thy Sun Nov 18 18:07:51 2018 +0000 @@ -197,7 +197,7 @@ finally show ?case . next case (Union I) - have *: "{Node l v r |l v r. (v, l, r) \<in> UNION UNIV I} = + have *: "{Node l v r |l v r. (v, l, r) \<in> \<Union>(I ` UNIV)} = (\<Union>i. {Node l v r |l v r. (v, l, r) \<in> I i})" by auto show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto qed