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