--- a/src/HOL/Probability/Probability.thy Thu Mar 18 14:52:11 2010 +0100
+++ b/src/HOL/Probability/Probability.thy Tue Mar 16 16:27:28 2010 +0100
@@ -1,5 +1,5 @@
theory Probability
-imports Probability_Space
+imports Probability_Space Product_Measure
begin
end