--- a/src/HOL/Library/Extended_Reals.thy Mon Mar 14 15:29:10 2011 +0100
+++ b/src/HOL/Library/Extended_Reals.thy Mon Mar 14 16:59:37 2011 +0100
@@ -1,8 +1,9 @@
-(* Title: src/HOL/Library/Extended_Reals.thy
- Author: Johannes Hölzl; TU München
- Author: Robert Himmelmann; TU München
- Author: Armin Heller; TU München
- Author: Bogdan Grechuk; University of Edinburgh *)
+(* Title: HOL/Library/Extended_Reals.thy
+ Author: Johannes Hölzl, TU München
+ Author: Robert Himmelmann, TU München
+ Author: Armin Heller, TU München
+ Author: Bogdan Grechuk, University of Edinburgh
+*)
header {* Extended real number line *}
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Mar 14 15:29:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Mar 14 16:59:37 2011 +0100
@@ -1,8 +1,9 @@
-(* Title: src/HOL/Multivariate_Analysis/Extended_Reals.thy
- Author: Johannes Hölzl; TU München
- Author: Robert Himmelmann; TU München
- Author: Armin Heller; TU München
- Author: Bogdan Grechuk; University of Edinburgh *)
+(* Title: HOL/Multivariate_Analysis/Extended_Real_Limits.thy
+ Author: Johannes Hölzl, TU München
+ Author: Robert Himmelmann, TU München
+ Author: Armin Heller, TU München
+ Author: Bogdan Grechuk, University of Edinburgh
+*)
header {* Limits on the Extended real number line *}
--- a/src/HOL/Probability/Complete_Measure.thy Mon Mar 14 15:29:10 2011 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Mon Mar 14 16:59:37 2011 +0100
@@ -1,6 +1,7 @@
-(* Title: Complete_Measure.thy
+(* Title: HOL/Probability/Complete_Measure.thy
Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen
*)
+
theory Complete_Measure
imports Product_Measure
begin
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Mar 14 15:29:10 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Mar 14 16:59:37 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: Sigma_Algebra.thy
+(* Title: HOL/Probability/Sigma_Algebra.thy
Author: Stefan Richter, Markus Wenzel, TU Muenchen
Plus material from the Hurd/Coble measure theory development,
translated by Lawrence Paulson.