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/Probability_Mass_Function.thy
changeset 61424 c3658c18b7bc
parent 61169 4de9ff3ea29a
child 61605 1bf7b186542e
child 61609 77b453bd616f 
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -163,7 +163,7 @@
 
   show ?thesis
     by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
-                                            unfolded pair_collapse] assms)
+                                            unfolded prod.collapse] assms)
         measurable
 qed
 
@@ -177,7 +177,7 @@
 
   show ?thesis
     by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
-                                            unfolded pair_collapse] assms)
+                                            unfolded prod.collapse] assms)
         measurable
 qed
isabelle