# HG changeset patch
# User hoelzl
# Date 1300820770 -3600
# Node ID 66c8281349ecc1ace84065b241d27e0bd580ad42
# Parent  6db76c88907a2737cc04b117def32b955ed4a9e2
standardized headers

diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,4 +1,7 @@
-(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(*  Title:      HOL/Probability/Lebesgue_Integration.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Armin Heller, TU München
+*)
 
 header {*Borel spaces*}
 
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Caratheodory.thy
--- 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" +
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,10 @@
+(*  Title:      HOL/Probability/Information.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Armin Heller, TU München
+*)
+
+header {*Information theory*}
+
 theory Information
 imports
   Probability_Space
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,4 +1,7 @@
-(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(*  Title:      HOL/Probability/Lebesgue_Integration.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Armin Heller, TU München
+*)
 
 header {*Lebesgue Integration*}
 
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,5 +1,10 @@
-(*  Author: Robert Himmelmann, TU Muenchen *)
+(*  Title:      HOL/Probability/Lebesgue_Measure.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Robert Himmelmann, TU München
+*)
+
 header {* Lebsegue measure *}
+
 theory Lebesgue_Measure
   imports Product_Measure
 begin
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,4 +1,10 @@
-(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(*  Title:      HOL/Probability/Measure.thy
+    Author:     Lawrence C Paulson
+    Author:     Johannes Hölzl, TU München
+    Author:     Armin Heller, TU München
+*)
+
+header {* Properties about measure spaces *}
 
 theory Measure
   imports Caratheodory
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,10 @@
+(*  Title:      HOL/Probability/Probability_Space.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Armin Heller, TU München
+*)
+
+header {*Probability spaces*}
+
 theory Probability_Space
 imports Lebesgue_Integration Radon_Nikodym Product_Measure
 begin
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Probability/Product_Measure.thy
+    Author:     Johannes Hölzl, TU München
+*)
+
+header {*Product measure spaces*}
+
 theory Product_Measure
 imports Lebesgue_Integration
 begin
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Probability/Radon_Nikodym.thy
+    Author:     Johannes Hölzl, TU München
+*)
+
+header {*Radon-Nikod{\'y}m derivative*}
+
 theory Radon_Nikodym
 imports Lebesgue_Integration
 begin
diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 20:06:10 2011 +0100
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Probability/Sigma_Algebra.thy
-    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
+    Author:     Stefan Richter, Markus Wenzel, TU München
+    Author:     Johannes Hölzl, TU München
     Plus material from the Hurd/Coble measure theory development,
     translated by Lawrence Paulson.
 *)