diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -130,7 +130,7 @@
     KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
     using f g ac by (subst density_density_divide) simp_all
   also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
-    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
+    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density)
   also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
     using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
   finally show ?thesis .
@@ -332,7 +332,7 @@
     from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
       by auto
     show "AE x in density M f. 0 \<le> g x / f x"
-      using f g by (auto simp: AE_density divide_nonneg_nonneg)
+      using f g by (auto simp: AE_density)
     show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
       using `1 < b` f g ac
       by (subst integral_density)
@@ -804,8 +804,7 @@
     using D
     apply (subst eq_commute)
     apply (intro RN_deriv_unique_sigma_finite)
-    apply (auto intro: divide_nonneg_nonneg measure_nonneg
-             simp: distributed_distr_eq_density[symmetric, OF X] sf)
+    apply (auto simp: distributed_distr_eq_density[symmetric, OF X] sf measure_nonneg)
     done
 qed
 
@@ -1102,7 +1101,7 @@
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
@@ -1115,7 +1114,7 @@
       "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
       by (subst positive_integral_multc)
-         (auto intro!: divide_nonneg_nonneg split: prod.split)
+         (auto split: prod.split)
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
@@ -1151,7 +1150,7 @@
     apply simp
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
@@ -1347,7 +1346,7 @@
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric])
@@ -1360,7 +1359,7 @@
     fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
       "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
-      by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
+      by (subst positive_integral_multc) auto
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
@@ -1396,7 +1395,7 @@
     apply (auto simp: split_beta') []
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"