--- a/src/HOL/Analysis/Sigma_Algebra.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Wed Jan 16 19:34:48 2019 -0500
@@ -5,7 +5,7 @@
translated by Lawrence Paulson.
*)
-section \<open>Sigma Algebra\<close>
+chapter \<open>Measure and Integration Theory\<close>
theory Sigma_Algebra
imports
@@ -17,6 +17,9 @@
"HOL-Library.Disjoint_Sets"
begin
+
+section \<open>Sigma Algebra\<close>
+
text \<open>Sigma algebras are an elementary concept in measure
theory. To measure --- that is to integrate --- functions, we first have
to measure sets. Unfortunately, when dealing with a large universe,