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/Analysis/Binary_Product_Measure.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
child 69517 dc20f278e8f3 
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -1118,7 +1118,7 @@
         unfolding * by auto
     next
       case (Union A)
-      moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
+      moreover have *: "(\<Union>(A ` UNIV)) \<times> UNIV = \<Union>((\<lambda>i. A i \<times> UNIV) ` UNIV)"
         by auto
       ultimately show ?case
         unfolding * by auto
@@ -1137,7 +1137,7 @@
         unfolding * by auto
     next
       case (Union B)
-      moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
+      moreover have *: "UNIV \<times> (\<Union>(B ` UNIV)) = \<Union>((\<lambda>i. UNIV \<times> B i) ` UNIV)"
         by auto
       ultimately show ?case
         unfolding * by auto
isabelle