src/HOL/Probability/Complete_Measure.thy
changeset 42146 5b52c6a9c627
parent 41983 2dc6e382a58b
child 42866 b0746bd57a41
     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Tue Mar 29 14:27:31 2011 +0200
     1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Tue Mar 29 14:27:39 2011 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  *)
     1.5  
     1.6  theory Complete_Measure
     1.7 -imports Product_Measure
     1.8 +imports Lebesgue_Integration
     1.9  begin
    1.10  
    1.11  locale completeable_measure_space = measure_space