--- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Mon Nov 09 15:48:17 2015 +0100
@@ -113,10 +113,10 @@
lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
using pmf.measure_pmf[of p] by auto
-interpretation measure_pmf!: prob_space "measure_pmf M" for M
+interpretation measure_pmf: prob_space "measure_pmf M" for M
by (rule prob_space_measure_pmf)
-interpretation measure_pmf!: subprob_space "measure_pmf M" for M
+interpretation measure_pmf: subprob_space "measure_pmf M" for M
by (rule prob_space_imp_subprob_space) unfold_locales
lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"