src/HOL/Probability/Lebesgue_Integration.thy

--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Jul 20 22:14:39 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jul 21 18:40:31 2011 +0200
@@ -6,7 +6,7 @@
 header {*Lebesgue Integration*}
 
 theory Lebesgue_Integration
-imports Measure Borel_Space
+  imports Measure Borel_Space
 begin
 
 lemma real_ereal_1[simp]: "real (1::ereal) = 1"