src/HOL/Probability/Information.thy
changeset 46905 6b1c0a80a57a
parent 46731 5302e932d1e5
child 47694 05663f75964c
     1.1 --- a/src/HOL/Probability/Information.thy	Tue Mar 13 16:40:06 2012 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Tue Mar 13 16:56:56 2012 +0100
     1.3 @@ -823,7 +823,7 @@
     1.4    interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
     1.5      using distribution_prob_space[OF X] .
     1.6    from A show "S.\<mu>' A = distribution X A"
     1.7 -    unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
     1.8 +    unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
     1.9  qed
    1.10  
    1.11  lemma (in information_space) entropy_uniform_max: