--- a/src/HOL/Probability/Caratheodory.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,9 +1,18 @@
+(* Title: HOL/Probability/Caratheodory.thy
+ Author: Lawrence C Paulson
+ Author: Johannes Hölzl, TU München
+*)
+
header {*Caratheodory Extension Theorem*}
theory Caratheodory
imports Sigma_Algebra Extended_Real_Limits
begin
+text {*
+ Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
+*}
+
lemma suminf_extreal_2dimen:
fixes f:: "nat \<times> nat \<Rightarrow> extreal"
assumes pos: "\<And>p. 0 \<le> f p"
@@ -36,8 +45,6 @@
SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg)
qed
-text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
-
subsection {* Measure Spaces *}
record 'a measure_space = "'a algebra" +