src/HOL/Probability/Information.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Probability/Information.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -945,7 +945,7 @@
     1.4    show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
     1.5      log b (measure MX A)"
     1.6      unfolding eq using uniform_distributed_params[OF X]
     1.7 -    by (subst lebesgue_integral_cmult) (auto simp: divide_minus_left measure_def)
     1.8 +    by (subst lebesgue_integral_cmult) (auto simp: measure_def)
     1.9  qed
    1.10  
    1.11  lemma (in information_space) entropy_simple_distributed: