src/HOL/Probability/Probability_Mass_Function.thy
changeset 61610 4f54d2759a0b
parent 61609 77b453bd616f
parent 61605 1bf7b186542e
child 61634 48e2de1b1df5
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Nov 10 14:18:41 2015 +0000
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Nov 10 14:43:29 2015 +0000
     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)"