standardized headers;
authorwenzelm
Mon, 14 Mar 2011 16:59:37 +0100
changeset 41983 2dc6e382a58b
parent 41982 96cbc6379e5a
child 41984 e5dba3d75e9e
standardized headers;
src/HOL/Library/Extended_Reals.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
--- 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.