diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,13 @@
 
 header {* Sigma Algebras *}
 
-theory Sigma_Algebra imports Main Countable FuncSet Indicator_Function begin
+theory Sigma_Algebra
+imports
+  Main
+  "~~/src/HOL/Library/Countable"
+  "~~/src/HOL/Library/FuncSet"
+  "~~/src/HOL/Library/Indicator_Function"
+begin
 
 text {* Sigma algebras are an elementary concept in measure
   theory. To measure --- that is to integrate --- functions, we first have