--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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}