changeset 61169 | 4de9ff3ea29a |
parent 60067 | f1a5bcf5658f |
child 61359 | e985b52c3eb3 |
--- a/src/HOL/Probability/Giry_Monad.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Sun Sep 13 22:56:52 2015 +0200 @@ -25,7 +25,7 @@ proof show "emeasure M (space M) \<noteq> \<infinity>" using * by auto qed - show "subprob_space M" by default fact+ + show "subprob_space M" by standard fact+ qed lemma prob_space_imp_subprob_space: