--- 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