modernized header;
authorwenzelm
Sun Nov 02 17:09:04 2014 +0100 (2014-11-02)
changeset 58877262572d90bc6
parent 58876 1888e3cb8048
child 58878 f962e42e324d
modernized header;
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Norm_Arith.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/PolyRoots.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/document/root.tex
     1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Nov 02 17:06:05 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Nov 02 17:09:04 2014 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  (*              (c) Copyright, John Harrison 1998-2008                       *)
     1.5  (* ========================================================================= *)
     1.6  
     1.7 -header {* Results connected with topological dimension. *}
     1.8 +section {* Results connected with topological dimension. *}
     1.9  
    1.10  theory Brouwer_Fixpoint
    1.11  imports Convex_Euclidean_Space
     2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
     2.5 +section {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
     2.6  
     2.7  theory Cartesian_Euclidean_Space
     2.8  imports Finite_Cartesian_Product Integration
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Nov 02 17:06:05 2014 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Nov 02 17:09:04 2014 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4      Ported from "hol_light/Multivariate/canal.ml" by L C Paulson (2014)
     3.5  *)
     3.6  
     3.7 -header {* Complex Analysis Basics *}
     3.8 +section {* Complex Analysis Basics *}
     3.9  
    3.10  theory Complex_Analysis_Basics
    3.11  imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Bogdan Grechuk, University of Edinburgh
     4.5  *)
     4.6  
     4.7 -header {* Convex sets, functions and related things. *}
     4.8 +section {* Convex sets, functions and related things. *}
     4.9  
    4.10  theory Convex_Euclidean_Space
    4.11  imports
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 02 17:06:05 2014 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 02 17:09:04 2014 +0100
     5.3 @@ -3,7 +3,7 @@
     5.4      Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
     5.5  *)
     5.6  
     5.7 -header {* Multivariate calculus in Euclidean space *}
     5.8 +section {* Multivariate calculus in Euclidean space *}
     5.9  
    5.10  theory Derivative
    5.11  imports Brouwer_Fixpoint Operator_Norm
     6.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Nov 02 17:06:05 2014 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Nov 02 17:09:04 2014 +0100
     6.3 @@ -2,7 +2,7 @@
     6.4      Author:     Amine Chaieb, University of Cambridge
     6.5  *)
     6.6  
     6.7 -header {* Traces, Determinant of square matrices and some properties *}
     6.8 +section {* Traces, Determinant of square matrices and some properties *}
     6.9  
    6.10  theory Determinants
    6.11  imports
     7.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
     7.3 @@ -3,7 +3,7 @@
     7.4      Author:     Brian Huffman, Portland State University
     7.5  *)
     7.6  
     7.7 -header {* Finite-Dimensional Inner Product Spaces *}
     7.8 +section {* Finite-Dimensional Inner Product Spaces *}
     7.9  
    7.10  theory Euclidean_Space
    7.11  imports
     8.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Nov 02 17:06:05 2014 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Nov 02 17:09:04 2014 +0100
     8.3 @@ -5,7 +5,7 @@
     8.4      Author:     Bogdan Grechuk, University of Edinburgh
     8.5  *)
     8.6  
     8.7 -header {* Limits on the Extended real number line *}
     8.8 +section {* Limits on the Extended real number line *}
     8.9  
    8.10  theory Extended_Real_Limits
    8.11    imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
     9.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Nov 02 17:06:05 2014 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Nov 02 17:09:04 2014 +0100
     9.3 @@ -2,7 +2,7 @@
     9.4      Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
     9.5  *)
     9.6  
     9.7 -header {* Fashoda meet theorem *}
     9.8 +section {* Fashoda meet theorem *}
     9.9  
    9.10  theory Fashoda
    9.11  imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
    10.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Nov 02 17:06:05 2014 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Nov 02 17:09:04 2014 +0100
    10.3 @@ -2,7 +2,7 @@
    10.4      Author:     Amine Chaieb, University of Cambridge
    10.5  *)
    10.6  
    10.7 -header {* Definition of finite Cartesian product types. *}
    10.8 +section {* Definition of finite Cartesian product types. *}
    10.9  
   10.10  theory Finite_Cartesian_Product
   10.11  imports
    11.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Nov 02 17:06:05 2014 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Nov 02 17:09:04 2014 +0100
    11.3 @@ -2,7 +2,7 @@
    11.4      Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
    11.5  *)
    11.6  
    11.7 -header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
    11.8 +section {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
    11.9  
   11.10  theory Integration
   11.11  imports
    12.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Nov 02 17:06:05 2014 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Nov 02 17:09:04 2014 +0100
    12.3 @@ -2,7 +2,7 @@
    12.4      Author:     Brian Huffman, Portland State University
    12.5  *)
    12.6  
    12.7 -header {* Square root of sum of squares *}
    12.8 +section {* Square root of sum of squares *}
    12.9  
   12.10  theory L2_Norm
   12.11  imports NthRoot
    13.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Nov 02 17:06:05 2014 +0100
    13.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Nov 02 17:09:04 2014 +0100
    13.3 @@ -2,7 +2,7 @@
    13.4      Author:     Amine Chaieb, University of Cambridge
    13.5  *)
    13.6  
    13.7 -header {* Elementary linear algebra on Euclidean spaces *}
    13.8 +section {* Elementary linear algebra on Euclidean spaces *}
    13.9  
   13.10  theory Linear_Algebra
   13.11  imports
    14.1 --- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Sun Nov 02 17:06:05 2014 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Sun Nov 02 17:09:04 2014 +0100
    14.3 @@ -2,7 +2,7 @@
    14.4      Author:     Amine Chaieb, University of Cambridge
    14.5  *)
    14.6  
    14.7 -header {* General linear decision procedure for normed spaces *}
    14.8 +section {* General linear decision procedure for normed spaces *}
    14.9  
   14.10  theory Norm_Arith
   14.11  imports "~~/src/HOL/Library/Sum_of_Squares"
    15.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Nov 02 17:06:05 2014 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Nov 02 17:09:04 2014 +0100
    15.3 @@ -3,7 +3,7 @@
    15.4      Author:     Brian Huffman
    15.5  *)
    15.6  
    15.7 -header {* Operator Norm *}
    15.8 +section {* Operator Norm *}
    15.9  
   15.10  theory Operator_Norm
   15.11  imports Complex_Main
    16.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Nov 02 17:06:05 2014 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Nov 02 17:09:04 2014 +0100
    16.3 @@ -2,7 +2,7 @@
    16.4      Author:     Robert Himmelmann, TU Muenchen
    16.5  *)
    16.6  
    16.7 -header {* Continuous paths and path-connected sets *}
    16.8 +section {* Continuous paths and path-connected sets *}
    16.9  
   16.10  theory Path_Connected
   16.11  imports Convex_Euclidean_Space
    17.1 --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sun Nov 02 17:06:05 2014 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sun Nov 02 17:09:04 2014 +0100
    17.3 @@ -1,4 +1,4 @@
    17.4 -header {* polynomial functions: extremal behaviour and root counts *}
    17.5 +section {* polynomial functions: extremal behaviour and root counts *}
    17.6  
    17.7  (*  Author: John Harrison and Valentina Bruno
    17.8      Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
    18.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
    18.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
    18.3 @@ -4,7 +4,7 @@
    18.4      Author:     Brian Huffman, Portland State University
    18.5  *)
    18.6  
    18.7 -header {* Elementary topology in Euclidean space. *}
    18.8 +section {* Elementary topology in Euclidean space. *}
    18.9  
   18.10  theory Topology_Euclidean_Space
   18.11  imports
    19.1 --- a/src/HOL/Multivariate_Analysis/document/root.tex	Sun Nov 02 17:06:05 2014 +0100
    19.2 +++ b/src/HOL/Multivariate_Analysis/document/root.tex	Sun Nov 02 17:09:04 2014 +0100
    19.3 @@ -23,8 +23,7 @@
    19.4  
    19.5  \newpage
    19.6  
    19.7 -\renewcommand{\isamarkupheader}[1]%
    19.8 -{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
    19.9 +\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
   19.10  
   19.11  \parindent 0pt\parskip 0.5ex
   19.12  \input{session}