summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)"