diff -r 8448713d48b7 -r 5b52c6a9c627 src/HOL/Probability/Complete_Measure.thy
--- 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