src/HOL/Probability/Probability_Mass_Function.thy
changeset 63040 eb4ddd18d635
parent 62975 1d066f6ab25d
child 63092 a949b2a5f51d
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -1138,7 +1138,9 @@
     1.4        from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
     1.5          and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
     1.6  
     1.7 -      def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
     1.8 +      define pr where "pr =
     1.9 +        bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy})
    1.10 +          (\<lambda>yz. return_pmf (fst xy, snd yz)))"
    1.11        have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    1.12          by (force simp: q')
    1.13