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

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