tuned style and headers
authornipkow
Fri Dec 28 10:29:59 2018 +0100 (4 months ago)
changeset 69517dc20f278e8f3
parent 69516 09bb8f470959
child 69518 bf88364c9e94
tuned style and headers
src/HOL/Analysis/Arcwise_Connected.thy
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Binary_Product_Measure.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Continuum_Not_Denumerable.thy
src/HOL/Analysis/Extended_Real_Limits.thy
src/HOL/Analysis/FPS_Convergence.thy
src/HOL/Analysis/Fashoda_Theorem.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Infinite_Set_Sum.thy
src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Lipschitz.thy
src/HOL/Analysis/Measurable.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Norm_Arith.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Poly_Roots.thy
src/HOL/Analysis/Radon_Nikodym.thy
src/HOL/Analysis/Simplex_Content.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Analysis/document/root.tex
     1.1 --- a/src/HOL/Analysis/Arcwise_Connected.thy	Thu Dec 27 23:38:55 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Fri Dec 28 10:29:59 2018 +0100
     1.3 @@ -2,11 +2,10 @@
     1.4      Authors:    LC Paulson, based on material from HOL Light
     1.5  *)
     1.6  
     1.7 -section \<open>Arcwise-connected sets\<close>
     1.8 +section \<open>Arcwise-Connected Sets\<close>
     1.9  
    1.10  theory Arcwise_Connected
    1.11 -  imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
    1.12 -
    1.13 +imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
    1.14  begin
    1.15  
    1.16  subsection%important \<open>The Brouwer reduction theorem\<close>
     2.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Thu Dec 27 23:38:55 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Fri Dec 28 10:29:59 2018 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4     Author:   Manuel Eberl, TU München
     2.5  *)
     2.6  
     2.7 -section \<open>The volume of an $n$-dimensional ball\<close>
     2.8 +section \<open>The Volume of an $n$-Dimensional Ball\<close>
     2.9  
    2.10  theory Ball_Volume
    2.11    imports Gamma_Function Lebesgue_Integral_Substitution
     3.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Johannes Hölzl, TU München
     3.5  *)
     3.6  
     3.7 -section%important \<open>Binary product measures\<close>
     3.8 +section%important \<open>Binary Product Measure\<close>
     3.9  
    3.10  theory Binary_Product_Measure
    3.11  imports Nonnegative_Lebesgue_Integration
     4.1 --- a/src/HOL/Analysis/Borel_Space.thy	Thu Dec 27 23:38:55 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Fri Dec 28 10:29:59 2018 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Armin Heller, TU München
     4.5  *)
     4.6  
     4.7 -section%important \<open>Borel spaces\<close>
     4.8 +section%important \<open>Borel Space\<close>
     4.9  
    4.10  theory Borel_Space
    4.11  imports
     5.1 --- a/src/HOL/Analysis/Caratheodory.thy	Thu Dec 27 23:38:55 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Fri Dec 28 10:29:59 2018 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  section%important \<open>Caratheodory Extension Theorem\<close>
     5.5  
     5.6  theory Caratheodory
     5.7 -  imports Measure_Space
     5.8 +imports Measure_Space
     5.9  begin
    5.10  
    5.11  text \<open>
     6.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Dec 27 23:38:55 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Dec 28 10:29:59 2018 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -section \<open>Complex path integrals and Cauchy's integral theorem\<close>
     6.5 +section \<open>Complex Path Integrals and Cauchy's Integral Theorem\<close>
     6.6  
     6.7  text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
     6.8  
     7.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Thu Dec 27 23:38:55 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Dec 28 10:29:59 2018 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -section \<open>Conformal Mappings and Consequences of Cauchy's integral theorem\<close>
     7.5 +section \<open>Conformal Mappings and Consequences of Cauchy's Integral Theorem\<close>
     7.6  
     7.7  text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>
     7.8  
     8.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Thu Dec 27 23:38:55 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Dec 28 10:29:59 2018 +0100
     8.3 @@ -3,7 +3,7 @@
     8.4      Author:     Johannes Hölzl, TU München
     8.5  *)
     8.6  
     8.7 -section \<open>Non-denumerability of the Continuum\<close>
     8.8 +section \<open>Non-Denumerability of the Continuum\<close>
     8.9  
    8.10  theory Continuum_Not_Denumerable
    8.11  imports
     9.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Dec 27 23:38:55 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Dec 28 10:29:59 2018 +0100
     9.3 @@ -5,7 +5,7 @@
     9.4      Author:     Bogdan Grechuk, University of Edinburgh
     9.5  *)
     9.6  
     9.7 -section%important \<open>Limits on the Extended real number line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
     9.8 +section%important \<open>Limits on the Extended Real Number Line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
     9.9  topics together? *)
    9.10  
    9.11  theory Extended_Real_Limits
    10.1 --- a/src/HOL/Analysis/FPS_Convergence.thy	Thu Dec 27 23:38:55 2018 +0100
    10.2 +++ b/src/HOL/Analysis/FPS_Convergence.thy	Fri Dec 28 10:29:59 2018 +0100
    10.3 @@ -5,7 +5,8 @@
    10.4    Connection of formal power series and actual convergent power series on Banach spaces
    10.5    (most notably the complex numbers).
    10.6  *)
    10.7 -section \<open>Convergence of formal power series\<close>
    10.8 +section \<open>Convergence of Formal Power Series\<close>
    10.9 +
   10.10  theory FPS_Convergence
   10.11  imports
   10.12    Conformal_Mappings
    11.1 --- a/src/HOL/Analysis/Fashoda_Theorem.thy	Thu Dec 27 23:38:55 2018 +0100
    11.2 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Fri Dec 28 10:29:59 2018 +0100
    11.3 @@ -2,7 +2,7 @@
    11.4      Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
    11.5  *)
    11.6  
    11.7 -section%important \<open>Fashoda meet theorem\<close>
    11.8 +section%important \<open>Fashoda Meet Theorem\<close>
    11.9  
   11.10  theory Fashoda_Theorem
   11.11  imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
    12.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 27 23:38:55 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Dec 28 10:29:59 2018 +0100
    12.3 @@ -2,7 +2,7 @@
    12.4      Author:     Amine Chaieb, University of Cambridge
    12.5  *)
    12.6  
    12.7 -section%important \<open>Definition of finite Cartesian product types\<close>
    12.8 +section%important \<open>Definition of Finite Cartesian Product Type\<close>
    12.9  
   12.10  theory Finite_Cartesian_Product
   12.11  imports
    13.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
    13.3 @@ -2,7 +2,7 @@
    13.4      Author:     Johannes Hölzl, TU München
    13.5  *)
    13.6  
    13.7 -section%important \<open>Finite product measures\<close>
    13.8 +section%important \<open>Finite Product Measure\<close>
    13.9  
   13.10  theory Finite_Product_Measure
   13.11  imports Binary_Product_Measure
    14.1 --- a/src/HOL/Analysis/Function_Topology.thy	Thu Dec 27 23:38:55 2018 +0100
    14.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Fri Dec 28 10:29:59 2018 +0100
    14.3 @@ -7,7 +7,7 @@
    14.4  begin
    14.5  
    14.6  
    14.7 -section%important \<open>Product topology\<close>
    14.8 +section%important \<open>Product Topology\<close>
    14.9  
   14.10  text \<open>We want to define the product topology.
   14.11  
    15.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 23:38:55 2018 +0100
    15.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Dec 28 10:29:59 2018 +0100
    15.3 @@ -3,11 +3,12 @@
    15.4                  Huge cleanup by LCP
    15.5  *)
    15.6  
    15.7 -section \<open>Henstock-Kurzweil gauge integration in many dimensions\<close>
    15.8 +section \<open>Henstock-Kurzweil Gauge Integration in Many Dimensions\<close>
    15.9  
   15.10  theory Henstock_Kurzweil_Integration
   15.11  imports
   15.12 -  Lebesgue_Measure Tagged_Division
   15.13 +  Lebesgue_Measure
   15.14 +  Tagged_Division
   15.15  begin
   15.16  
   15.17  lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
    16.1 --- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Dec 27 23:38:55 2018 +0100
    16.2 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Fri Dec 28 10:29:59 2018 +0100
    16.3 @@ -4,7 +4,8 @@
    16.4  
    16.5    A theory of sums over possible infinite sets. (Only works for absolute summability)
    16.6  *)
    16.7 -section \<open>Sums over infinite sets\<close>
    16.8 +section \<open>Sums over Infinite Sets\<close>
    16.9 +
   16.10  theory Infinite_Set_Sum
   16.11    imports Set_Integral
   16.12  begin
    17.1 --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Dec 27 23:38:55 2018 +0100
    17.2 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Fri Dec 28 10:29:59 2018 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4      This could probably be weakened somehow.
    17.5  *)
    17.6  
    17.7 -section \<open>Integration by Substition for the Lebesgue integral\<close>
    17.8 +section \<open>Integration by Substition for the Lebesgue Integral\<close>
    17.9  
   17.10  theory Lebesgue_Integral_Substitution
   17.11  imports Interval_Integral
    18.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
    18.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
    18.3 @@ -5,10 +5,15 @@
    18.4      Author:     Luke Serafin
    18.5  *)
    18.6  
    18.7 -section \<open>Lebesgue measure\<close>
    18.8 +section \<open>Lebesgue Measure\<close>
    18.9  
   18.10  theory Lebesgue_Measure
   18.11 -  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity
   18.12 +imports
   18.13 +  Finite_Product_Measure
   18.14 +  Caratheodory
   18.15 +  Complete_Measure
   18.16 +  Summation_Tests
   18.17 +  Regularity
   18.18  begin
   18.19  
   18.20  lemma measure_eqI_lessThan:
    19.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 23:38:55 2018 +0100
    19.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Dec 28 10:29:59 2018 +0100
    19.3 @@ -2,7 +2,7 @@
    19.4      Author:     Amine Chaieb, University of Cambridge
    19.5  *)
    19.6  
    19.7 -section \<open>Elementary linear algebra on Euclidean spaces\<close>
    19.8 +section \<open>Elementary Linear Algebra on Euclidean Spaces\<close>
    19.9  
   19.10  theory Linear_Algebra
   19.11  imports
    20.1 --- a/src/HOL/Analysis/Lipschitz.thy	Thu Dec 27 23:38:55 2018 +0100
    20.2 +++ b/src/HOL/Analysis/Lipschitz.thy	Fri Dec 28 10:29:59 2018 +0100
    20.3 @@ -2,9 +2,10 @@
    20.4      Author:     Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    20.5      Author:     Fabian Immler, TU München
    20.6  *)
    20.7 -section \<open>Lipschitz continuity\<close>
    20.8 +section \<open>Lipschitz Continuity\<close>
    20.9 +
   20.10  theory Lipschitz
   20.11 -  imports Borel_Space
   20.12 +imports Borel_Space
   20.13  begin
   20.14  
   20.15  definition%important lipschitz_on
    21.1 --- a/src/HOL/Analysis/Measurable.thy	Thu Dec 27 23:38:55 2018 +0100
    21.2 +++ b/src/HOL/Analysis/Measurable.thy	Fri Dec 28 10:29:59 2018 +0100
    21.3 @@ -1,7 +1,7 @@
    21.4  (*  Title:      HOL/Analysis/Measurable.thy
    21.5      Author:     Johannes Hölzl <hoelzl@in.tum.de>
    21.6  *)
    21.7 -section \<open>Measurability prover\<close>
    21.8 +section \<open>Measurability Prover\<close>
    21.9  theory Measurable
   21.10    imports
   21.11      Sigma_Algebra
    22.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Dec 27 23:38:55 2018 +0100
    22.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Dec 28 10:29:59 2018 +0100
    22.3 @@ -4,7 +4,7 @@
    22.4      Author:     Armin Heller, TU München
    22.5  *)
    22.6  
    22.7 -section \<open>Measure spaces and their properties\<close>
    22.8 +section \<open>Measure Spaces\<close>
    22.9  
   22.10  theory Measure_Space
   22.11  imports
    23.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Thu Dec 27 23:38:55 2018 +0100
    23.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Dec 28 10:29:59 2018 +0100
    23.3 @@ -2,7 +2,7 @@
    23.4      Author:     Amine Chaieb, University of Cambridge
    23.5  *)
    23.6  
    23.7 -section \<open>General linear decision procedure for normed spaces\<close>
    23.8 +section \<open>Linear Decision Procedure for Normed Spaces\<close>
    23.9  
   23.10  theory Norm_Arith
   23.11  imports "HOL-Library.Sum_of_Squares"
    24.1 --- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 27 23:38:55 2018 +0100
    24.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Fri Dec 28 10:29:59 2018 +0100
    24.3 @@ -2,7 +2,7 @@
    24.4      Authors:    LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
    24.5  *)
    24.6  
    24.7 -section \<open>Continuous paths and path-connected sets\<close>
    24.8 +section \<open>Continuous Paths and Path-Connected Sets\<close>
    24.9  
   24.10  theory Path_Connected
   24.11    imports Continuous_Extension Continuum_Not_Denumerable
   24.12 @@ -2530,7 +2530,7 @@
   24.13    by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq assms)
   24.14  
   24.15  
   24.16 -section\<open>The \<open>inside\<close> and \<open>outside\<close> of a set\<close>
   24.17 +section\<open>The \<open>inside\<close> and \<open>outside\<close> of a Set\<close>
   24.18  
   24.19  text%important\<open>The inside comprises the points in a bounded connected component of the set's complement.
   24.20    The outside comprises the points in unbounded connected component of the complement.\<close>
    25.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Thu Dec 27 23:38:55 2018 +0100
    25.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Fri Dec 28 10:29:59 2018 +0100
    25.3 @@ -2,7 +2,7 @@
    25.4      Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
    25.5  *)
    25.6  
    25.7 -section%important \<open>polynomial functions: extremal behaviour and root counts\<close>
    25.8 +section%important \<open>Polynomial Functions: Extremal Behaviour and Root Counts\<close>
    25.9  
   25.10  theory Poly_Roots
   25.11  imports Complex_Main
    26.1 --- a/src/HOL/Analysis/Radon_Nikodym.thy	Thu Dec 27 23:38:55 2018 +0100
    26.2 +++ b/src/HOL/Analysis/Radon_Nikodym.thy	Fri Dec 28 10:29:59 2018 +0100
    26.3 @@ -2,7 +2,7 @@
    26.4      Author:     Johannes Hölzl, TU München
    26.5  *)
    26.6  
    26.7 -section%important \<open>Radon-Nikod{\'y}m derivative\<close>
    26.8 +section%important \<open>Radon-Nikod{\'y}m Derivative\<close>
    26.9  
   26.10  theory Radon_Nikodym
   26.11  imports Bochner_Integration
    27.1 --- a/src/HOL/Analysis/Simplex_Content.thy	Thu Dec 27 23:38:55 2018 +0100
    27.2 +++ b/src/HOL/Analysis/Simplex_Content.thy	Fri Dec 28 10:29:59 2018 +0100
    27.3 @@ -5,9 +5,10 @@
    27.4     The content of an n-dimensional simplex, including the formula for the content of a
    27.5     triangle and Heron's formula.
    27.6  *)
    27.7 -section%important \<open>Volume of a simplex\<close>
    27.8 +section%important \<open>Volume of a Simplex\<close>
    27.9 +
   27.10  theory Simplex_Content
   27.11 -  imports Change_Of_Vars
   27.12 +imports Change_Of_Vars
   27.13  begin
   27.14  
   27.15  lemma fact_neq_top_ennreal [simp]: "fact n \<noteq> (top :: ennreal)"
    28.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Dec 27 23:38:55 2018 +0100
    28.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Fri Dec 28 10:29:59 2018 +0100
    28.3 @@ -1,4 +1,4 @@
    28.4 -section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
    28.5 +section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close>
    28.6  
    28.7  text\<open>By L C Paulson (2015)\<close>
    28.8  
    29.1 --- a/src/HOL/Analysis/document/root.tex	Thu Dec 27 23:38:55 2018 +0100
    29.2 +++ b/src/HOL/Analysis/document/root.tex	Fri Dec 28 10:29:59 2018 +0100
    29.3 @@ -10,7 +10,7 @@
    29.4  \usepackage{pdfsetup}
    29.5  
    29.6  \urlstyle{rm}
    29.7 -\isabellestyle{it}
    29.8 +\isabellestyle{literalunderscore}
    29.9  \pagestyle{myheadings}
   29.10  
   29.11  \begin{document}
   29.12 @@ -26,7 +26,7 @@
   29.13  
   29.14  \newpage
   29.15  
   29.16 -\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
   29.17 +\renewcommand{\setisabellecontext}[1]{\markright{#1.thy}}
   29.18  
   29.19  \parindent 0pt\parskip 0.5ex
   29.20  \input{session}