# HG changeset patch
# User nipkow
# Date 1545989399 -3600
# Node ID dc20f278e8f36d6f2fd8b2019fd86818f2518968
# Parent  09bb8f47095988d0879e18dbdb05f0d23fa3c8bd
tuned style and headers

diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,11 +2,10 @@
     Authors:    LC Paulson, based on material from HOL Light
 *)
 
-section \<open>Arcwise-connected sets\<close>
+section \<open>Arcwise-Connected Sets\<close>
 
 theory Arcwise_Connected
-  imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
-
+imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
 begin
 
 subsection%important \<open>The Brouwer reduction theorem\<close>
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Ball_Volume.thy
--- a/src/HOL/Analysis/Ball_Volume.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -3,7 +3,7 @@
    Author:   Manuel Eberl, TU München
 *)
 
-section \<open>The volume of an $n$-dimensional ball\<close>
+section \<open>The Volume of an $n$-Dimensional Ball\<close>
 
 theory Ball_Volume
   imports Gamma_Function Lebesgue_Integral_Substitution
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section%important \<open>Binary product measures\<close>
+section%important \<open>Binary Product Measure\<close>
 
 theory Binary_Product_Measure
 imports Nonnegative_Lebesgue_Integration
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -3,7 +3,7 @@
     Author:     Armin Heller, TU München
 *)
 
-section%important \<open>Borel spaces\<close>
+section%important \<open>Borel Space\<close>
 
 theory Borel_Space
 imports
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -6,7 +6,7 @@
 section%important \<open>Caratheodory Extension Theorem\<close>
 
 theory Caratheodory
-  imports Measure_Space
+imports Measure_Space
 begin
 
 text \<open>
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -1,4 +1,4 @@
-section \<open>Complex path integrals and Cauchy's integral theorem\<close>
+section \<open>Complex Path Integrals and Cauchy's Integral Theorem\<close>
 
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
 
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -1,4 +1,4 @@
-section \<open>Conformal Mappings and Consequences of Cauchy's integral theorem\<close>
+section \<open>Conformal Mappings and Consequences of Cauchy's Integral Theorem\<close>
 
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>
 
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -3,7 +3,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section \<open>Non-denumerability of the Continuum\<close>
+section \<open>Non-Denumerability of the Continuum\<close>
 
 theory Continuum_Not_Denumerable
 imports
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -5,7 +5,7 @@
     Author:     Bogdan Grechuk, University of Edinburgh
 *)
 
-section%important \<open>Limits on the Extended real number line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
+section%important \<open>Limits on the Extended Real Number Line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
 topics together? *)
 
 theory Extended_Real_Limits
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -5,7 +5,8 @@
   Connection of formal power series and actual convergent power series on Banach spaces
   (most notably the complex numbers).
 *)
-section \<open>Convergence of formal power series\<close>
+section \<open>Convergence of Formal Power Series\<close>
+
 theory FPS_Convergence
 imports
   Conformal_Mappings
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
 *)
 
-section%important \<open>Fashoda meet theorem\<close>
+section%important \<open>Fashoda Meet Theorem\<close>
 
 theory Fashoda_Theorem
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-section%important \<open>Definition of finite Cartesian product types\<close>
+section%important \<open>Definition of Finite Cartesian Product Type\<close>
 
 theory Finite_Cartesian_Product
 imports
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section%important \<open>Finite product measures\<close>
+section%important \<open>Finite Product Measure\<close>
 
 theory Finite_Product_Measure
 imports Binary_Product_Measure
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -7,7 +7,7 @@
 begin
 
 
-section%important \<open>Product topology\<close>
+section%important \<open>Product Topology\<close>
 
 text \<open>We want to define the product topology.
 
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -3,11 +3,12 @@
                 Huge cleanup by LCP
 *)
 
-section \<open>Henstock-Kurzweil gauge integration in many dimensions\<close>
+section \<open>Henstock-Kurzweil Gauge Integration in Many Dimensions\<close>
 
 theory Henstock_Kurzweil_Integration
 imports
-  Lebesgue_Measure Tagged_Division
+  Lebesgue_Measure
+  Tagged_Division
 begin
 
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -4,7 +4,8 @@
 
   A theory of sums over possible infinite sets. (Only works for absolute summability)
 *)
-section \<open>Sums over infinite sets\<close>
+section \<open>Sums over Infinite Sets\<close>
+
 theory Infinite_Set_Sum
   imports Set_Integral
 begin
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -6,7 +6,7 @@
     This could probably be weakened somehow.
 *)
 
-section \<open>Integration by Substition for the Lebesgue integral\<close>
+section \<open>Integration by Substition for the Lebesgue Integral\<close>
 
 theory Lebesgue_Integral_Substitution
 imports Interval_Integral
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -5,10 +5,15 @@
     Author:     Luke Serafin
 *)
 
-section \<open>Lebesgue measure\<close>
+section \<open>Lebesgue Measure\<close>
 
 theory Lebesgue_Measure
-  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity
+imports
+  Finite_Product_Measure
+  Caratheodory
+  Complete_Measure
+  Summation_Tests
+  Regularity
 begin
 
 lemma measure_eqI_lessThan:
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-section \<open>Elementary linear algebra on Euclidean spaces\<close>
+section \<open>Elementary Linear Algebra on Euclidean Spaces\<close>
 
 theory Linear_Algebra
 imports
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,9 +2,10 @@
     Author:     Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
     Author:     Fabian Immler, TU München
 *)
-section \<open>Lipschitz continuity\<close>
+section \<open>Lipschitz Continuity\<close>
+
 theory Lipschitz
-  imports Borel_Space
+imports Borel_Space
 begin
 
 definition%important lipschitz_on
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Measurable.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Analysis/Measurable.thy
     Author:     Johannes Hölzl <hoelzl@in.tum.de>
 *)
-section \<open>Measurability prover\<close>
+section \<open>Measurability Prover\<close>
 theory Measurable
   imports
     Sigma_Algebra
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -4,7 +4,7 @@
     Author:     Armin Heller, TU München
 *)
 
-section \<open>Measure spaces and their properties\<close>
+section \<open>Measure Spaces\<close>
 
 theory Measure_Space
 imports
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Norm_Arith.thy
--- a/src/HOL/Analysis/Norm_Arith.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-section \<open>General linear decision procedure for normed spaces\<close>
+section \<open>Linear Decision Procedure for Normed Spaces\<close>
 
 theory Norm_Arith
 imports "HOL-Library.Sum_of_Squares"
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Authors:    LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
 *)
 
-section \<open>Continuous paths and path-connected sets\<close>
+section \<open>Continuous Paths and Path-Connected Sets\<close>
 
 theory Path_Connected
   imports Continuous_Extension Continuum_Not_Denumerable
@@ -2530,7 +2530,7 @@
   by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq assms)
 
 
-section\<open>The \<open>inside\<close> and \<open>outside\<close> of a set\<close>
+section\<open>The \<open>inside\<close> and \<open>outside\<close> of a Set\<close>
 
 text%important\<open>The inside comprises the points in a bounded connected component of the set's complement.
   The outside comprises the points in unbounded connected component of the complement.\<close>
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Poly_Roots.thy
--- a/src/HOL/Analysis/Poly_Roots.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
 *)
 
-section%important \<open>polynomial functions: extremal behaviour and root counts\<close>
+section%important \<open>Polynomial Functions: Extremal Behaviour and Root Counts\<close>
 
 theory Poly_Roots
 imports Complex_Main
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section%important \<open>Radon-Nikod{\'y}m derivative\<close>
+section%important \<open>Radon-Nikod{\'y}m Derivative\<close>
 
 theory Radon_Nikodym
 imports Bochner_Integration
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Simplex_Content.thy
--- a/src/HOL/Analysis/Simplex_Content.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Simplex_Content.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -5,9 +5,10 @@
    The content of an n-dimensional simplex, including the formula for the content of a
    triangle and Heron's formula.
 *)
-section%important \<open>Volume of a simplex\<close>
+section%important \<open>Volume of a Simplex\<close>
+
 theory Simplex_Content
-  imports Change_Of_Vars
+imports Change_Of_Vars
 begin
 
 lemma fact_neq_top_ennreal [simp]: "fact n \<noteq> (top :: ennreal)"
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -1,4 +1,4 @@
-section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
+section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close>
 
 text\<open>By L C Paulson (2015)\<close>
 
diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/document/root.tex
--- a/src/HOL/Analysis/document/root.tex	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/document/root.tex	Fri Dec 28 10:29:59 2018 +0100
@@ -10,7 +10,7 @@
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
-\isabellestyle{it}
+\isabellestyle{literalunderscore}
 \pagestyle{myheadings}
 
 \begin{document}
@@ -26,7 +26,7 @@
 
 \newpage
 
-\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
+\renewcommand{\setisabellecontext}[1]{\markright{#1.thy}}
 
 \parindent 0pt\parskip 0.5ex
 \input{session}