src/HOL/Probability/Probability.thy
changeset 42148 d596e7bb251f
parent 42147 61d5d50ca74c
child 42861 16375b493b64
--- a/src/HOL/Probability/Probability.thy	Tue Mar 29 14:27:41 2011 +0200
+++ b/src/HOL/Probability/Probability.thy	Tue Mar 29 14:27:42 2011 +0200
@@ -2,7 +2,7 @@
 imports
   Complete_Measure
   Lebesgue_Measure
-  Probability
+  Probability_Measure
   Infinite_Product_Measure
   Information
   "ex/Dining_Cryptographers"