src/HOL/Probability/Probability_Mass_Function.thy
changeset 61605 1bf7b186542e
parent 61424 c3658c18b7bc
child 61610 4f54d2759a0b
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 09 13:49:56 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 09 15:48:17 2015 +0100
     1.3 @@ -113,10 +113,10 @@
     1.4  lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
     1.5    using pmf.measure_pmf[of p] by auto
     1.6  
     1.7 -interpretation measure_pmf!: prob_space "measure_pmf M" for M
     1.8 +interpretation measure_pmf: prob_space "measure_pmf M" for M
     1.9    by (rule prob_space_measure_pmf)
    1.10  
    1.11 -interpretation measure_pmf!: subprob_space "measure_pmf M" for M
    1.12 +interpretation measure_pmf: subprob_space "measure_pmf M" for M
    1.13    by (rule prob_space_imp_subprob_space) unfold_locales
    1.14  
    1.15  lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"