modernized header;

--- a/src/HOL/NSA/CLim.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/CLim.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-header{*Limits, Continuity and Differentiation for Complex Functions*}
+section{*Limits, Continuity and Differentiation for Complex Functions*}
 
 theory CLim
 imports CStar

--- a/src/HOL/NSA/CStar.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/CStar.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   : 2001 University of Edinburgh
 *)
 
-header{*Star-transforms in NSA, Extending Sets of Complex Numbers
+section{*Star-transforms in NSA, Extending Sets of Complex Numbers
       and Complex Functions*}
 
 theory CStar

--- a/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-header{*The Nonstandard Primes as an Extension of the Prime Numbers*}
+section{*The Nonstandard Primes as an Extension of the Prime Numbers*}
 
 theory NSPrimes
 imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal"

--- a/src/HOL/NSA/Filter.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/Filter.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Brian Huffman
 *) 
 
-header {* Filters and Ultrafilters *}
+section {* Filters and Ultrafilters *}
 
 theory Filter
 imports "~~/src/HOL/Library/Infinite_Set"

--- a/src/HOL/NSA/HDeriv.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HDeriv.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-header{* Differentiation (Nonstandard) *}
+section{* Differentiation (Nonstandard) *}
 
 theory HDeriv
 imports HLim

--- a/src/HOL/NSA/HLim.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HLim.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson
 *)
 
-header{* Limits and Continuity (Nonstandard) *}
+section{* Limits and Continuity (Nonstandard) *}
 
 theory HLim
 imports Star

--- a/src/HOL/NSA/HLog.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HLog.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   : 2000,2001 University of Edinburgh
 *)
 
-header{*Logarithms: Non-Standard Version*}
+section{*Logarithms: Non-Standard Version*}
 
 theory HLog
 imports HTranscendental

--- a/src/HOL/NSA/HSEQ.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HSEQ.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -6,7 +6,7 @@
     Additional contributions by Jeremy Avigad and Brian Huffman
 *)
 
-header {* Sequences and Convergence (Nonstandard) *}
+section {* Sequences and Convergence (Nonstandard) *}
 
 theory HSEQ
 imports Limits NatStar

--- a/src/HOL/NSA/HSeries.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HSeries.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -5,7 +5,7 @@
 Converted to Isar and polished by lcp    
 *) 
 
-header{*Finite Summation and Infinite Series for Hyperreals*}
+section{*Finite Summation and Infinite Series for Hyperreals*}
 
 theory HSeries
 imports HSEQ

--- a/src/HOL/NSA/HTranscendental.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HTranscendental.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -5,7 +5,7 @@
 Converted to Isar and polished by lcp
 *)
 
-header{*Nonstandard Extensions of Transcendental Functions*}
+section{*Nonstandard Extensions of Transcendental Functions*}
 
 theory HTranscendental
 imports Transcendental HSeries HDeriv

--- a/src/HOL/NSA/HyperDef.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-header{*Construction of Hyperreals Using Ultrafilters*}
+section{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
 imports Complex_Main HyperNat

--- a/src/HOL/NSA/HyperNat.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HyperNat.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -5,7 +5,7 @@
 Converted to Isar and polished by lcp    
 *)
 
-header{*Hypernatural numbers*}
+section{*Hypernatural numbers*}
 
 theory HyperNat
 imports StarDef

--- a/src/HOL/NSA/NSA.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/NSA.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, University of Cambridge
 *)
 
-header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
+section{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
 theory NSA
 imports HyperDef "~~/src/HOL/Library/Lub_Glb"

--- a/src/HOL/NSA/NSCA.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/NSCA.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   : 2001,2002 University of Edinburgh
 *)
 
-header{*Non-Standard Complex Analysis*}
+section{*Non-Standard Complex Analysis*}
 
 theory NSCA
 imports NSComplex HTranscendental

--- a/src/HOL/NSA/NSComplex.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson
 *)
 
-header{*Nonstandard Complex Numbers*}
+section{*Nonstandard Complex Numbers*}
 
 theory NSComplex
 imports NSA

--- a/src/HOL/NSA/NatStar.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/NatStar.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -5,7 +5,7 @@
 Converted to Isar and polished by lcp
 *)
 
-header{*Star-transforms for the Hypernaturals*}
+section{*Star-transforms for the Hypernaturals*}
 
 theory NatStar
 imports Star

--- a/src/HOL/NSA/Star.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/Star.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
 *)
 
-header{*Star-Transforms in Non-Standard Analysis*}
+section{*Star-Transforms in Non-Standard Analysis*}
 
 theory Star
 imports NSA

--- a/src/HOL/NSA/StarDef.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/StarDef.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -2,7 +2,7 @@
     Author      : Jacques D. Fleuriot and Brian Huffman
 *)
 
-header {* Construction of Star Types Using Ultrafilters *}
+section {* Construction of Star Types Using Ultrafilters *}
 
 theory StarDef
 imports Filter

--- a/src/HOL/NSA/document/root.tex	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/document/root.tex	Sun Nov 02 17:13:28 2014 +0100
@@ -19,8 +19,7 @@
 
 \newpage
 
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
 
 \parindent 0pt\parskip 0.5ex
 \input{session}