diff -r f51985ebd152 -r 19b7ace1c5da src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Jun 13 07:05:01 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Fri Jun 13 14:08:20 2014 +0200
@@ -8,7 +8,6 @@
 theory Information
 imports
   Independent_Family
-  Distributions
   "~~/src/HOL/Library/Convex"
 begin
 
@@ -916,35 +915,6 @@
     by (subst integral_mult_right) (auto simp: measure_def)
 qed
 
-lemma (in information_space) entropy_exponential:
-  assumes D: "distributed M lborel X (exponential_density l)"
-  shows "entropy b lborel X = log b (exp 1 / l)"
-proof -
-  have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
- 
-  have [simp]: "integrable lborel (exponential_density l)"
-    using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
-
-  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
-    using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
-    
-  have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
-    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
-
-  have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
-    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
-    
-  have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
-    using D by (rule entropy_distr)
-  also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
-    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
-    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
-  also have "\<dots> = (ln l - 1) / ln b"
-    by simp
-  finally show ?thesis
-    by (simp add: log_def divide_simps ln_div)
-qed
-
 lemma (in information_space) entropy_simple_distributed:
   "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
   by (subst entropy_distr[OF simple_distributed])