--- 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>
--- 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
--- 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
--- 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
--- 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>
--- 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>
--- 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>
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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.
--- 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>
--- 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
--- 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
--- 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:
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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>
--- 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
--- 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
--- 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)"
--- 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>
--- 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}