# HG changeset patch
# User wenzelm
# Date 1414944365 -3600
# Node ID 1888e3cb8048750014c914d0529090283eb1ae5e
# Parent  ab1c65b015c35f14f0c42f373015ebd162d9911f
modernized header;

diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {*Binary product measures*}
+section {*Binary product measures*}
 
 theory Binary_Product_Measure
 imports Nonnegative_Lebesgue_Integration
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {* Bochner Integration for Vector-Valued Functions *}
+section {* Bochner Integration for Vector-Valued Functions *}
 
 theory Bochner_Integration
   imports Finite_Product_Measure
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Armin Heller, TU München
 *)
 
-header {*Borel spaces*}
+section {*Borel spaces*}
 
 theory Borel_Space
 imports
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {*Caratheodory Extension Theorem*}
+section {*Caratheodory Extension Theorem*}
 
 theory Caratheodory
   imports Measure_Space
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Convolution.thy
--- a/src/HOL/Probability/Convolution.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Convolution.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Sudeep Kanav, TU München
     Author:     Johannes Hölzl, TU München *)
 
-header {* Convolution Measure *}
+section {* Convolution Measure *}
 
 theory Convolution
   imports Independent_Family
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Distributions.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Johannes Hölzl, TU München
     Author:     Jeremy Avigad, CMU *)
 
-header {* Properties of Various Distributions *}
+section {* Properties of Various Distributions *}
 
 theory Distributions
   imports Convolution Information
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU München
 *)
 
-header {* Finite Maps *}
+section {* Finite Maps *}
 
 theory Fin_Map
 imports Finite_Product_Measure
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {*Finite product measures*}
+section {*Finite product measures*}
 
 theory Finite_Product_Measure
 imports Binary_Product_Measure
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Sudeep Kanav, TU München
 *)
 
-header {* Independent families of events, event sets, and random variables *}
+section {* Independent families of events, event sets, and random variables *}
 
 theory Independent_Family
   imports Probability_Measure Infinite_Product_Measure
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {*Infinite Product Measure*}
+section {*Infinite Product Measure*}
 
 theory Infinite_Product_Measure
   imports Probability_Measure Caratheodory Projective_Family
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Information.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Armin Heller, TU München
 *)
 
-header {*Information theory*}
+section {*Information theory*}
 
 theory Information
 imports
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -5,7 +5,7 @@
     Author:     Luke Serafin
 *)
 
-header {* Lebsegue measure *}
+section {* Lebsegue measure *}
 
 theory Lebesgue_Measure
   imports Finite_Product_Measure Bochner_Integration Caratheodory
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Armin Heller, TU München
 *)
 
-header {* Measure spaces and their properties *}
+section {* Measure spaces and their properties *}
 
 theory Measure_Space
 imports
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Armin Heller, TU München
 *)
 
-header {* Lebesgue Integration for Nonnegative Functions *}
+section {* Lebesgue Integration for Nonnegative Functions *}
 
 theory Nonnegative_Lebesgue_Integration
   imports Measure_Space Borel_Space
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Armin Heller, TU München
 *)
 
-header {*Probability measure*}
+section {*Probability measure*}
 
 theory Probability_Measure
   imports Lebesgue_Measure Radon_Nikodym
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {*Projective Family*}
+section {*Projective Family*}
 
 theory Projective_Family
 imports Finite_Product_Measure Probability_Measure
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU München
 *)
 
-header {* Projective Limit *}
+section {* Projective Limit *}
 
 theory Projective_Limit
   imports
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {*Radon-Nikod{\'y}m derivative*}
+section {*Radon-Nikod{\'y}m derivative*}
 
 theory Radon_Nikodym
 imports Bochner_Integration
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Regularity.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU München
 *)
 
-header {* Regularity of Measures *}
+section {* Regularity of Measures *}
 
 theory Regularity
 imports Measure_Space Borel_Space
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -5,7 +5,7 @@
     translated by Lawrence Paulson.
 *)
 
-header {* Describing measurable sets *}
+section {* Describing measurable sets *}
 
 theory Sigma_Algebra
 imports
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/document/root.tex
--- a/src/HOL/Probability/document/root.tex	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/document/root.tex	Sun Nov 02 17:06:05 2014 +0100
@@ -23,8 +23,7 @@
   \includegraphics[scale=0.45]{session_graph}
 \end{center}
 
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
 
 \parindent 0pt\parskip 0.5ex
 \input{session}
diff -r ab1c65b015c3 -r 1888e3cb8048 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Nov 02 16:59:40 2014 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Nov 02 17:06:05 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Johannes Hölzl, TU München *)
 
-header {* Formalization of a Countermeasure by Koepf \& Duermuth 2009 *}
+section {* Formalization of a Countermeasure by Koepf \& Duermuth 2009 *}
 
 theory Koepf_Duermuth_Countermeasure
   imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation"