src/HOL/Probability/Giry_Monad.thy

--- a/src/HOL/Probability/Giry_Monad.thy	Wed Nov 11 10:13:40 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Wed Nov 11 10:28:22 2015 +0100
@@ -1567,4 +1567,8 @@
   by (rule measure_eqI) 
      (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
 
+lemma null_measure_in_space_subprob_algebra [simp]:
+  "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}"
+by(simp add: space_subprob_algebra subprob_space_null_measure_iff)
+
 end