# HG changeset patch
# User wenzelm
# Date 1414944544 -3600
# Node ID 262572d90bc68972422096fb60a1e47b76764a0a
# Parent  1888e3cb8048750014c914d0529090283eb1ae5e
modernized header;

diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -16,7 +16,7 @@
 (*              (c) Copyright, John Harrison 1998-2008                       *)
 (* ========================================================================= *)
 
-header {* Results connected with topological dimension. *}
+section {* Results connected with topological dimension. *}
 
 theory Brouwer_Fixpoint
 imports Convex_Euclidean_Space
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -1,4 +1,4 @@
-header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
+section {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
 
 theory Cartesian_Euclidean_Space
 imports Finite_Cartesian_Product Integration
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Ported from "hol_light/Multivariate/canal.ml" by L C Paulson (2014)
 *)
 
-header {* Complex Analysis Basics *}
+section {* Complex Analysis Basics *}
 
 theory Complex_Analysis_Basics
 imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Bogdan Grechuk, University of Edinburgh
 *)
 
-header {* Convex sets, functions and related things. *}
+section {* Convex sets, functions and related things. *}
 
 theory Convex_Euclidean_Space
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
 *)
 
-header {* Multivariate calculus in Euclidean space *}
+section {* Multivariate calculus in Euclidean space *}
 
 theory Derivative
 imports Brouwer_Fixpoint Operator_Norm
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header {* Traces, Determinant of square matrices and some properties *}
+section {* Traces, Determinant of square matrices and some properties *}
 
 theory Determinants
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-header {* Finite-Dimensional Inner Product Spaces *}
+section {* Finite-Dimensional Inner Product Spaces *}
 
 theory Euclidean_Space
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -5,7 +5,7 @@
     Author:     Bogdan Grechuk, University of Edinburgh
 *)
 
-header {* Limits on the Extended real number line *}
+section {* Limits on the Extended real number line *}
 
 theory Extended_Real_Limits
   imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
 *)
 
-header {* Fashoda meet theorem *}
+section {* Fashoda meet theorem *}
 
 theory Fashoda
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header {* Definition of finite Cartesian product types. *}
+section {* Definition of finite Cartesian product types. *}
 
 theory Finite_Cartesian_Product
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
 *)
 
-header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
+section {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
 
 theory Integration
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-header {* Square root of sum of squares *}
+section {* Square root of sum of squares *}
 
 theory L2_Norm
 imports NthRoot
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header {* Elementary linear algebra on Euclidean spaces *}
+section {* Elementary linear algebra on Euclidean spaces *}
 
 theory Linear_Algebra
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Norm_Arith.thy
--- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header {* General linear decision procedure for normed spaces *}
+section {* General linear decision procedure for normed spaces *}
 
 theory Norm_Arith
 imports "~~/src/HOL/Library/Sum_of_Squares"
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Operator Norm *}
+section {* Operator Norm *}
 
 theory Operator_Norm
 imports Complex_Main
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Robert Himmelmann, TU Muenchen
 *)
 
-header {* Continuous paths and path-connected sets *}
+section {* Continuous paths and path-connected sets *}
 
 theory Path_Connected
 imports Convex_Euclidean_Space
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -1,4 +1,4 @@
-header {* polynomial functions: extremal behaviour and root counts *}
+section {* polynomial functions: extremal behaviour and root counts *}
 
 (*  Author: John Harrison and Valentina Bruno
     Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-header {* Elementary topology in Euclidean space. *}
+section {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
 imports
diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/document/root.tex
--- a/src/HOL/Multivariate_Analysis/document/root.tex	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/document/root.tex	Sun Nov 02 17:09:04 2014 +0100
@@ -23,8 +23,7 @@
 
 \newpage
 
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
 
 \parindent 0pt\parskip 0.5ex
 \input{session}