src/HOL/Probability/Information.thy

     apply (rule log_setsum')
     using not_empty b_gt_1 finite_space sum_over_space_real_distribution
     by auto
   also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?d x \<noteq> 0 then 1 else 0)"
     apply (rule arg_cong[where f="\<lambda>f. log b (\<Sum>x\<in>X`space M. f x)"])
-    using distribution_finite[of X] by (auto simp: ext_iff real_of_pinfreal_eq_0)
+    using distribution_finite[of X] by (auto simp: fun_eq_iff real_of_pinfreal_eq_0)
   finally show ?thesis
     using finite_space by (auto simp: setsum_cases real_eq_of_nat)
 qed
 
 lemma (in finite_information_space) entropy_uniform_max:

   let "?dYZ A" = "real (joint_distribution Y Z A)"
   let "?dX A" = "real (distribution X A)"
   let "?dZ A" = "real (distribution Z A)"
   let ?M = "X ` space M \<times> Y ` space M \<times> Z ` space M"
 
-  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: ext_iff)
+  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: fun_eq_iff)
 
   have "- (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
     log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))
     \<le> log b (\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})"
     unfolding split_beta