src/HOL/Probability/Probability_Measure.thy
changeset 50002 ce0d316b5b44
parent 50001 382bd3173584
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     1.3 @@ -876,7 +876,7 @@
     1.4      then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
     1.5      with A a X have "emeasure (distr M S X) {a} = P' a"
     1.6        by (subst emeasure_distr)
     1.7 -         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure
     1.8 +         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
     1.9                 intro!: arg_cong[where f=prob])
    1.10      also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
    1.11        using A X a
    1.12 @@ -934,7 +934,7 @@
    1.13  lemma simple_distributed_simple_function:
    1.14    "simple_distributed M X Px \<Longrightarrow> simple_function M X"
    1.15    unfolding simple_distributed_def distributed_def
    1.16 -  by (auto simp: simple_function_def)
    1.17 +  by (auto simp: simple_function_def measurable_count_space_eq2)
    1.18  
    1.19  lemma simple_distributed_measure:
    1.20    "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"