diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Mon Oct 03 14:09:26 2016 +0100
+++ b/src/HOL/Probability/Information.thy	Fri Sep 30 16:08:38 2016 +0200
@@ -389,10 +389,6 @@
     done
 qed
 
-lemma integrable_cong_AE_imp:
-  "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
-  using integrable_cong_AE[of f M g] by (auto simp: eq_commute)
-
 lemma (in information_space) finite_entropy_integrable:
   "finite_entropy S X Px \<Longrightarrow> integrable S (\<lambda>x. Px x * log b (Px x))"
   unfolding finite_entropy_def by auto