Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Tree_Space.thy
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
isabelle