src/HOL/Probability/Probability_Mass_Function.thy
changeset 61169 4de9ff3ea29a
parent 60602 37588fbe39f9
child 61424 c3658c18b7bc
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -653,7 +653,7 @@
     measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
     by (simp add: AE_density nonneg measure_def emeasure_density max_def)
   show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
-    by default (simp add: emeasure_density prob)
+    by standard (simp add: emeasure_density prob)
 qed simp
 
 lemma pmf_embed_pmf: "pmf embed_pmf x = f x"