src/HOL/Probability/Information.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 40859 de0b30e6c2d2
     1.1 --- a/src/HOL/Probability/Information.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Probability/Information.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -505,7 +505,7 @@
     1.4      by auto
     1.5    also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?d x \<noteq> 0 then 1 else 0)"
     1.6      apply (rule arg_cong[where f="\<lambda>f. log b (\<Sum>x\<in>X`space M. f x)"])
     1.7 -    using distribution_finite[of X] by (auto simp: ext_iff real_of_pinfreal_eq_0)
     1.8 +    using distribution_finite[of X] by (auto simp: fun_eq_iff real_of_pinfreal_eq_0)
     1.9    finally show ?thesis
    1.10      using finite_space by (auto simp: setsum_cases real_eq_of_nat)
    1.11  qed
    1.12 @@ -645,7 +645,7 @@
    1.13    let "?dZ A" = "real (distribution Z A)"
    1.14    let ?M = "X ` space M \<times> Y ` space M \<times> Z ` space M"
    1.15  
    1.16 -  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: ext_iff)
    1.17 +  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: fun_eq_iff)
    1.18  
    1.19    have "- (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
    1.20      log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))