--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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}
--- 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"