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