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})))
```