changeset 47762 | d31085f07f60 |
parent 47761 | dfe747e72fa8 |
child 49773 | 16907431e477 |
--- a/src/HOL/Probability/Measure_Space.thy Wed Apr 25 19:26:00 2012 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Wed Apr 25 19:26:27 2012 +0200 @@ -636,7 +636,7 @@ unfolding null_sets_def by simp interpretation null_sets: ring_of_sets "space M" "null_sets M" for M -proof +proof (rule ring_of_setsI) show "null_sets M \<subseteq> Pow (space M)" using sets_into_space by auto show "{} \<in> null_sets M"