changeset 42146 | 5b52c6a9c627 |
parent 41983 | 2dc6e382a58b |
child 42866 | b0746bd57a41 |
--- a/src/HOL/Probability/Complete_Measure.thy Tue Mar 29 14:27:31 2011 +0200 +++ b/src/HOL/Probability/Complete_Measure.thy Tue Mar 29 14:27:39 2011 +0200 @@ -3,7 +3,7 @@ *) theory Complete_Measure -imports Product_Measure +imports Lebesgue_Integration begin locale completeable_measure_space = measure_space