src/HOL/Probability/Information.thy
changeset 50002 ce0d316b5b44
parent 49999 dfb63b9b8908
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Information.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:40 2012 +0100
     1.3 @@ -446,7 +446,7 @@
     1.4    shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
     1.5    using assms unfolding finite_entropy_def
     1.6    using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
     1.7 -  by (auto intro: distributed_real_measurable)
     1.8 +  by (auto dest!: distributed_real_measurable)
     1.9  
    1.10  subsection {* Mutual Information *}
    1.11  
    1.12 @@ -1578,7 +1578,7 @@
    1.13    have "random_variable (count_space (X ` space M)) X"
    1.14      by (simp add: comp_def)
    1.15    then have "simple_function M X"    
    1.16 -    unfolding simple_function_def by auto
    1.17 +    unfolding simple_function_def by (auto simp: measurable_count_space_eq2)
    1.18    then have "simple_distributed M X ?Px"
    1.19      by (rule simple_distributedI) auto
    1.20    then show "distributed M (count_space (X ` space M)) X ?Px"