# HG changeset patch
# User wenzelm
# Date 1414945245 -3600
# Node ID b9556a0556324eb9481e7a15a076241002eec504
# Parent  0baae4311a9f715a72050052bf4ec2a96276b5b4
modernized header;

diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/AList.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
 *)
 
-header {* Implementation of Association Lists *}
+section {* Implementation of Association Lists *}
 
 theory AList
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/AList_Mapping.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
    Author: Florian Haftmann, TU Muenchen
 *)
 
-header {* Implementation of mappings with Association Lists *}
+section {* Implementation of mappings with Association Lists *}
 
 theory AList_Mapping
 imports AList Mapping
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/BNF_Axiomatization.thy
--- a/src/HOL/Library/BNF_Axiomatization.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
 Axiomatic declaration of bounded natural functors.
 *)
 
-header {* Axiomatic declaration of Bounded Natural Functors *}
+section {* Axiomatic declaration of Bounded Natural Functors *}
 
 theory BNF_Axiomatization
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/BigO.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Authors:    Jeremy Avigad and Kevin Donnelly
 *)
 
-header {* Big O notation *}
+section {* Big O notation *}
 
 theory BigO
 imports Complex_Main Function_Algebras Set_Algebras
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Bit.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The Field of Integers mod 2 *}
+section {* The Field of Integers mod 2 *}
 
 theory Bit
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Boolean Algebras *}
+section {* Boolean Algebras *}
 
 theory Boolean_Algebra
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Cardinal_Notations.thy
--- a/src/HOL/Library/Cardinal_Notations.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Cardinal_Notations.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
 Cardinal notations.
 *)
 
-header {* Cardinal Notations *}
+section {* Cardinal Notations *}
 
 theory Cardinal_Notations
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Cardinality.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman, Andreas Lochbihler
 *)
 
-header {* Cardinality of types *}
+section {* Cardinality of types *}
 
 theory Cardinality
 imports Phantom_Type
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Char_ord.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Norbert Voelker, Florian Haftmann
 *)
 
-header {* Order on characters *}
+section {* Order on characters *}
 
 theory Char_ord
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
 *)
 
-header {* Avoidance of pattern matching on natural numbers *}
+section {* Avoidance of pattern matching on natural numbers *}
 
 theory Code_Abstract_Nat
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Implementation of natural numbers as binary numerals *}
+section {* Implementation of natural numbers as binary numerals *}
 
 theory Code_Binary_Nat
 imports Code_Abstract_Nat
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Char.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann
 *)
 
-header {* Code generation of pretty characters (and strings) *}
+section {* Code generation of pretty characters (and strings) *}
 
 theory Code_Char
 imports Main Char_ord
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Prolog.thy
--- a/src/HOL/Library/Code_Prolog.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Prolog.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lukas Bulwahn, TUM 2010
 *)
 
-header {* Code generation of prolog programs *}
+section {* Code generation of prolog programs *}
 
 theory Code_Prolog
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Implementation of integer numbers by target-language integers *}
+section {* Implementation of integer numbers by target-language integers *}
 
 theory Code_Target_Int
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Implementation of natural numbers by target-language integers *}
+section {* Implementation of natural numbers by target-language integers *}
 
 theory Code_Target_Nat
 imports Code_Abstract_Nat
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Code_Target_Numeral.thy
--- a/src/HOL/Library/Code_Target_Numeral.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Target_Numeral.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Implementation of natural and integer numbers by target-language integers *}
+section {* Implementation of natural and integer numbers by target-language integers *}
 
 theory Code_Target_Numeral
 imports Code_Target_Int Code_Target_Nat
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {* Non-denumerability of the Continuum. *}
+section {* Non-denumerability of the Continuum. *}
 
 theory ContNotDenum
 imports Complex_Main Countable_Set
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Convex.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Johannes Hoelzl, TU Muenchen
 *)
 
-header {* Convexity in real vector spaces *}
+section {* Convexity in real vector spaces *}
 
 theory Convex
 imports Product_Vector
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Countable.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
 *)
 
-header {* Encoding (almost) everything into natural numbers *}
+section {* Encoding (almost) everything into natural numbers *}
 
 theory Countable
 imports Old_Datatype Rat Nat_Bijection
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Andrei Popescu
 *)
 
-header {* Countable sets *}
+section {* Countable sets *}
 
 theory Countable_Set
 imports Countable Infinite_Set
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
 Type of (at most) countable sets.
 *)
 
-header {* Type of (at Most) Countable Sets *}
+section {* Type of (at Most) Countable Sets *}
 
 theory Countable_Set_Type
 imports Countable_Set Cardinal_Notations
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/DAList.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
-header \<open>Abstract type of association lists with unique keys\<close>
+section \<open>Abstract type of association lists with unique keys\<close>
 
 theory DAList
 imports AList
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
-header \<open>Multisets partially implemented by association lists\<close>
+section \<open>Multisets partially implemented by association lists\<close>
 
 theory DAList_Multiset
 imports Multiset DAList
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Debug.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Debugging facilities for code generated towards Isabelle/ML *}
+section {* Debugging facilities for code generated towards Isabelle/ML *}
 
 theory Debug
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Diagonal_Subsequence.thy
--- a/src/HOL/Library/Diagonal_Subsequence.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Diagonal_Subsequence.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Fabian Immler, TUM *)
 
-header {* Sequence of Properties on Subsequences *}
+section {* Sequence of Properties on Subsequences *}
 
 theory Diagonal_Subsequence
 imports Complex_Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Discrete.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)  
 
-header {* Common discrete functions *}
+section {* Common discrete functions *}
 
 theory Discrete
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Dlist.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Lists with elements distinct as canonical example for datatype invariants *}
+section {* Lists with elements distinct as canonical example for datatype invariants *}
 
 theory Dlist
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Contributions: David Trachtenherz, TU Muenchen
 *)
 
-header {* Extended natural numbers (i.e. with infinity) *}
+section {* Extended natural numbers (i.e. with infinity) *}
 
 theory Extended_Nat
 imports Main Countable
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
     Author:     Bogdan Grechuk, University of Edinburgh
 *)
 
-header {* Extended real number line *}
+section {* Extended real number line *}
 
 theory Extended_Real
 imports Complex_Main Extended_Nat Liminf_Limsup
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Andrei Popescu, TU Muenchen
 *)
 
-header {* Type of finite sets defined as a subtype of sets *}
+section {* Type of finite sets defined as a subtype of sets *}
 
 theory FSet
 imports Conditionally_Complete_Lattices
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FinFun.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
 
-header {* Almost everywhere constant functions *}
+section {* Almost everywhere constant functions *}
 
 theory FinFun
 imports Cardinality
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/FinFun_Syntax.thy
--- a/src/HOL/Library/FinFun_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FinFun_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Andreas Lochbihler, KIT *)
 
-header {* Pretty syntax for almost everywhere constant functions *}
+section {* Pretty syntax for almost everywhere constant functions *}
 
 theory FinFun_Syntax
 imports FinFun
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Float.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2012  TU München
 *)
 
-header {* Floating-Point Numbers *}
+section {* Floating-Point Numbers *}
 
 theory Float
 imports Complex_Main Lattice_Algebras
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header{* A formalization of formal power series *}
+section{* A formalization of formal power series *}
 
 theory Formal_Power_Series
 imports "~~/src/HOL/Number_Theory/Binomial"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header{* A formalization of the fraction field of any integral domain;
+section{* A formalization of the fraction field of any integral domain;
          generalization of theory Rat from int to any integral domain *}
 
 theory Fraction_Field
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Fun_Lexorder.thy
--- a/src/HOL/Library/Fun_Lexorder.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Fun_Lexorder.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header \<open>Lexical order on functions\<close>
+section \<open>Lexical order on functions\<close>
 
 theory Fun_Lexorder
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FuncSet.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
 *)
 
-header \<open>Pi and Function Sets\<close>
+section \<open>Pi and Function Sets\<close>
 
 theory FuncSet
 imports Hilbert_Choice Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
 *)
 
-header {* Pointwise instantiation of functions to algebra type classes *}
+section {* Pointwise instantiation of functions to algebra type classes *}
 
 theory Function_Algebras
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Function_Division.thy
--- a/src/HOL/Library/Function_Division.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Function_Division.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TUM
 *)
 
-header {* Pointwise instantiation of functions to division *}
+section {* Pointwise instantiation of functions to division *}
 
 theory Function_Division
 imports Function_Algebras
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Function_Growth.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,7 +1,7 @@
 
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Comparing growth of functions on natural numbers by a preorder relation *}
+section {* Comparing growth of functions on natural numbers by a preorder relation *}
 
 theory Function_Growth
 imports Main Preorder Discrete
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Amine Chaieb, TU Muenchen *)
 
-header{*Fundamental Theorem of Algebra*}
+section{*Fundamental Theorem of Algebra*}
 
 theory Fundamental_Theorem_Algebra
 imports Polynomial Complex_Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header \<open>Big sum and product over function bodies\<close>
+section \<open>Big sum and product over function bodies\<close>
 
 theory Groups_Big_Fun
 imports
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/IArray.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,4 +1,4 @@
-header "Immutable Arrays with Code Generation"
+section "Immutable Arrays with Code Generation"
 
 theory IArray
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hoelzl (TU Muenchen)
 *)
 
-header {* Indicator Function *}
+section {* Indicator Function *}
 
 theory Indicator_Function
 imports Complex_Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Stephan Merz
 *)
 
-header {* Infinite Sets and Related Concepts *}
+section {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Inner Product Spaces and the Gradient Derivative *}
+section {* Inner Product Spaces and the Gradient Derivative *}
 
 theory Inner_Product
 imports "~~/src/HOL/Complex_Main"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Steven Obua, TU Muenchen *)
 
-header {* Various algebraic structures combined with a lattice *}
+section {* Various algebraic structures combined with a lattice *}
 
 theory Lattice_Algebras
 imports Complex_Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Lattice_Syntax.thy
--- a/src/HOL/Library/Lattice_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Pretty syntax for lattice operations *}
+section {* Pretty syntax for lattice operations *}
 
 theory Lattice_Syntax
 imports Complete_Lattices
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-header {* Liminf and Limsup on complete lattices *}
+section {* Liminf and Limsup on complete lattices *}
 
 theory Liminf_Limsup
 imports Complex_Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Dmitriy Traytel, TU Muenchen
 *)
 
-header {* Linear Temporal Logic on Streams *}
+section {* Linear Temporal Logic on Streams *}
 
 theory Linear_Temporal_Logic_on_Streams
   imports Stream Sublist
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/ListVector.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (*  Author: Tobias Nipkow, 2007 *)
 
-header {* Lists as vectors *}
+section {* Lists as vectors *}
 
 theory ListVector
 imports List Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/List_lexord.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Norbert Voelker
 *)
 
-header {* Lexicographic order on lists *}
+section {* Lexicographic order on lists *}
 
 theory List_lexord
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Lub_Glb.thy
--- a/src/HOL/Library/Lub_Glb.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Lub_Glb.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Jacques D. Fleuriot, University of Cambridge
     Author:     Amine Chaieb, University of Cambridge *)
 
-header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
+section {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
 
 theory Lub_Glb
 imports Complex_Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann and Ondrej Kuncar
 *)
 
-header {* An abstract view on maps for code generation. *}
+section {* An abstract view on maps for code generation. *}
 
 theory Mapping
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
    Author: Christian Sternagel, University of Innsbruck
 *)
 
-header {* Monad notation for arbitrary types *}
+section {* Monad notation for arbitrary types *}
 
 theory Monad_Syntax
 imports Main "~~/src/Tools/Adhoc_Overloading"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/More_List.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,7 +1,7 @@
 (* Author: Andreas Lochbihler, ETH Zürich
    Author: Florian Haftmann, TU Muenchen  *)
 
-header \<open>Less common functions on lists\<close>
+section \<open>Less common functions on lists\<close>
 
 theory More_List
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Andrei Popescu, TU Muenchen
 *)
 
-header {* (Finite) multisets *}
+section {* (Finite) multisets *}
 
 theory Multiset
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -6,7 +6,7 @@
     Author:     Alexander Krauss
 *)
 
-header {* Bijections between natural numbers and other types *}
+section {* Bijections between natural numbers and other types *}
 
 theory Nat_Bijection
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Numeral Syntax for Types *}
+section {* Numeral Syntax for Types *}
 
 theory Numeral_Type
 imports Cardinality
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 *)
 
-header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
+section {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
 
 theory Old_Datatype
 imports "../Main"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Old_Recdef.thy
--- a/src/HOL/Library/Old_Recdef.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Konrad Slind and Markus Wenzel, TU Muenchen
 *)
 
-header {* TFL: recursive function definitions *}
+section {* TFL: recursive function definitions *}
 
 theory Old_Recdef
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Old_SMT.thy
--- a/src/HOL/Library/Old_SMT.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Old_SMT.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Sascha Boehme, TU Muenchen
 *)
 
-header {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
+section {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
 
 theory Old_SMT
 imports "../Real" "../Word/Word"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Option_ord.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Canonical order on option type *}
+section {* Canonical order on option type *}
 
 theory Option_ord
 imports Option Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Order_Continuity.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-header {* Continuity and iterations (of set transformers) *}
+section {* Continuity and iterations (of set transformers) *}
 
 theory Order_Continuity
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Parallel.thy
--- a/src/HOL/Library/Parallel.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Parallel.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Futures and parallel lists for code generated towards Isabelle/ML *}
+section {* Futures and parallel lists for code generated towards Isabelle/ML *}
 
 theory Parallel
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Permutation.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
 *)
 
-header {* Permutations *}
+section {* Permutations *}
 
 theory Permutation
 imports Multiset
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Permutations.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header {* Permutations, both general and specifically on finite sets.*}
+section {* Permutations, both general and specifically on finite sets.*}
 
 theory Permutations
 imports Fact
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Phantom_Type.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Andreas Lochbihler
 *)
 
-header {* A generic phantom type *}
+section {* A generic phantom type *}
 
 theory Phantom_Type
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header{* Polynomials and Differentiation *}
+section{* Polynomials and Differentiation *}
 
 theory Poly_Deriv
 imports Deriv Polynomial
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Florian Haftmann
 *)
 
-header {* Polynomials as type over a ring structure *}
+section {* Polynomials as type over a ring structure *}
 
 theory Polynomial
 imports Main GCD "~~/src/HOL/Library/More_List"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Lukas Bulwahn, TU Muenchen *)
 
-header {* A Prototype of Quickcheck based on the Predicate Compiler *}
+section {* A Prototype of Quickcheck based on the Predicate Compiler *}
 
 theory Predicate_Compile_Quickcheck
 imports Main Predicate_Compile_Alternative_Defs
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Prefix_Order.thy
--- a/src/HOL/Library/Prefix_Order.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Prefix_Order.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 *)
 
-header {* Prefix order on lists as order class instance *}
+section {* Prefix order on lists as order class instance *}
 
 theory Prefix_Order
 imports Sublist
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Preorder.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Florian Haftmann, TU Muenchen *)
 
-header {* Preorders with explicit equivalence relation *}
+section {* Preorders with explicit equivalence relation *}
 
 theory Preorder
 imports Orderings
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Product_Lexorder.thy
--- a/src/HOL/Library/Product_Lexorder.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_Lexorder.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Norbert Voelker
 *)
 
-header {* Lexicographic order on product types *}
+section {* Lexicographic order on product types *}
 
 theory Product_Lexorder
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Pointwise order on product types *}
+section {* Pointwise order on product types *}
 
 theory Product_Order
 imports Product_plus Conditionally_Complete_Lattices
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Cartesian Products as Vector Spaces *}
+section {* Cartesian Products as Vector Spaces *}
 
 theory Product_Vector
 imports Inner_Product Product_plus
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_plus.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Additive group operations on product types *}
+section {* Additive group operations on product types *}
 
 theory Product_plus
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-header {* Quotient infrastructure for the list type *}
+section {* Quotient infrastructure for the list type *}
 
 theory Quotient_List
 imports Main Quotient_Set Quotient_Product Quotient_Option
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-header {* Quotient infrastructure for the option type *}
+section {* Quotient infrastructure for the option type *}
 
 theory Quotient_Option
 imports Main Quotient_Syntax
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-header {* Quotient infrastructure for the product type *}
+section {* Quotient infrastructure for the product type *}
 
 theory Quotient_Product
 imports Main Quotient_Syntax
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Set.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-header {* Quotient infrastructure for the set type *}
+section {* Quotient infrastructure for the set type *}
 
 theory Quotient_Set
 imports Main Quotient_Syntax
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-header {* Quotient infrastructure for the sum type *}
+section {* Quotient infrastructure for the sum type *}
 
 theory Quotient_Sum
 imports Main Quotient_Syntax
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_Syntax.thy
--- a/src/HOL/Library/Quotient_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-header {* Pretty syntax for Quotient operations *}
+section {* Pretty syntax for Quotient operations *}
 
 theory Quotient_Syntax
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Type.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
-header {* Quotient types *}
+section {* Quotient types *}
 
 theory Quotient_Type
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lukas Bulwahn and Ondrej Kuncar
 *)
 
-header {* Abstract type of RBT trees *}
+section {* Abstract type of RBT trees *}
 
 theory RBT 
 imports Main RBT_Impl
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header {* Implementation of Red-Black Trees *}
+section {* Implementation of Red-Black Trees *}
 
 theory RBT_Impl
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/RBT_Mapping.thy
--- a/src/HOL/Library/RBT_Mapping.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann and Ondrej Kuncar
 *)
 
-header {* Implementation of mappings with Red-Black Trees *}
+section {* Implementation of mappings with Red-Black Trees *}
 
 (*<*)
 theory RBT_Mapping
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Ondrej Kuncar
 *)
 
-header {* Implementation of sets using RBT trees *}
+section {* Implementation of sets using RBT trees *}
 
 theory RBT_Set
 imports RBT Product_Lexorder
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Ramsey.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tom Ridge.  Converted to structured Isar by L C Paulson
 *)
 
-header "Ramsey's Theorem"
+section "Ramsey's Theorem"
 
 theory Ramsey
 imports Main Infinite_Set
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Reflection.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
-header {* Generic reflection and reification *}
+section {* Generic reflection and reification *}
 
 theory Reflection
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Refute.thy
--- a/src/HOL/Library/Refute.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Refute.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
 Basic setup and documentation for the 'refute' (and 'refute_params') command.
 *)
 
-header {* Refute *}
+section {* Refute *}
 
 theory Refute
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Saturated.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
     Author:     Florian Haftmann
 *)
 
-header {* Saturated arithmetic *}
+section {* Saturated arithmetic *}
 
 theory Saturated
 imports Numeral_Type "~~/src/HOL/Word/Type_Length"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Set_Algebras.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
 *)
 
-header {* Algebraic operations on sets *}
+section {* Algebraic operations on sets *}
 
 theory Set_Algebras
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/State_Monad.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
+section {* Combinator syntax for generic, open state monads (single-threaded monads) *}
 
 theory State_Monad
 imports Main Monad_Syntax
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Stream.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -6,7 +6,7 @@
 Infinite streams.
 *)
 
-header {* Infinite Streams *}
+section {* Infinite Streams *}
 
 theory Stream
 imports "~~/src/HOL/Library/Nat_Bijection"
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sublist.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Christian Sternagel, JAIST
 *)
 
-header {* List prefixes, suffixes, and homeomorphic embedding *}
+section {* List prefixes, suffixes, and homeomorphic embedding *}
 
 theory Sublist
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
                 Florian Haftmann, Tobias Nipkow, TU Muenchen
 *)
 
-header {* Sublist Ordering *}
+section {* Sublist Ordering *}
 
 theory Sublist_Order
 imports Sublist
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Sum_of_Squares.thy
--- a/src/HOL/Library/Sum_of_Squares.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Philipp Meyer, TU Muenchen
 *)
 
-header {* A decision procedure for universal multivariate real arithmetic
+section {* A decision procedure for universal multivariate real arithmetic
   with addition, multiplication and ordering using semidefinite programming *}
 
 theory Sum_of_Squares
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Sum_of_Squares_Remote.thy
--- a/src/HOL/Library/Sum_of_Squares_Remote.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sum_of_Squares_Remote.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Philipp Meyer, TU Muenchen
 *)
 
-header {* Examples with remote CSDP *}
+section {* Examples with remote CSDP *}
 
 theory Sum_of_Squares_Remote
 imports Sum_of_Squares
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
 
-header {* A table-based implementation of the reflexive transitive closure *}
+section {* A table-based implementation of the reflexive transitive closure *}
 
 theory Transitive_Closure_Table
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Tree.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-header {* Binary Tree *}
+section {* Binary Tree *}
 
 theory Tree
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss
 *)
 
-header {* A general ``while'' combinator *}
+section {* A general ``while'' combinator *}
 
 theory While_Combinator
 imports Main
diff -r 0baae4311a9f -r b9556a055632 src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/document/root.tex	Sun Nov 02 17:20:45 2014 +0100
@@ -18,9 +18,7 @@
 \tableofcontents
 \newpage
 
-\renewcommand{\isamarkupheader}[1]%
-{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
-\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
 
 \input{session}