# HG changeset patch
# User wenzelm
# Date 1414942794 -3600
# Node ID c399ae4b836f677709a5efaec5cb57410cad0c54
# Parent  e2c0d8ef29cbe78dac32e24c35dc12445bea4373
modernized header;

diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/AC.thy
--- a/src/ZF/AC.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/AC.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*The Axiom of Choice*}
+section{*The Axiom of Choice*}
 
 theory AC imports Main_ZF begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Arith.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
   Also, rec(m, 0, %z w.z) is pred(m).
 *)
 
-header{*Arithmetic Operators and Their Definitions*}
+section{*Arithmetic Operators and Their Definitions*}
 
 theory Arith imports Univ begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ArithSimp.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000  University of Cambridge
 *)
 
-header{*Arithmetic with simplification*}
+section{*Arithmetic with simplification*}
 
 theory ArithSimp
 imports Arith
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Bin.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -13,7 +13,7 @@
 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
 *)
 
-header{*Arithmetic on Binary Integers*}
+section{*Arithmetic on Binary Integers*}
 
 theory Bin
 imports Int_ZF Datatype_ZF
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Bool.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1992  University of Cambridge
 *)
 
-header{*Booleans in Zermelo-Fraenkel Set Theory*}
+section{*Booleans in Zermelo-Fraenkel Set Theory*}
 
 theory Bool imports pair begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Cardinal.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Cardinal Numbers Without the Axiom of Choice*}
+section{*Cardinal Numbers Without the Axiom of Choice*}
 
 theory Cardinal imports OrderType Finite Nat_ZF Sum begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/CardinalArith.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Cardinal Arithmetic Without the Axiom of Choice*}
+section{*Cardinal Arithmetic Without the Axiom of Choice*}
 
 theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Cardinal_AC.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
 These results help justify infinite-branching datatypes
 *)
 
-header{*Cardinal Arithmetic Using AC*}
+section{*Cardinal Arithmetic Using AC*}
 
 theory Cardinal_AC imports CardinalArith Zorn begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {* The Axiom of Choice Holds in L! *}
+section {* The Axiom of Choice Holds in L! *}
 
 theory AC_in_L imports Formula Separation begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Absoluteness for the Definable Powerset Function*}
+section {*Absoluteness for the Definable Powerset Function*}
 
 
 theory DPow_absolute imports Satisfies_absolute begin
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Absoluteness Properties for Recursive Datatypes*}
+section {*Absoluteness Properties for Recursive Datatypes*}
 
 theory Datatype_absolute imports Formula WF_absolute begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Formula.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {* First-Order Formulas and the Definition of the Class L *}
+section {* First-Order Formulas and the Definition of the Class L *}
 
 theory Formula imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {* The ZF Axioms (Except Separation) in L *}
+section {* The ZF Axioms (Except Separation) in L *}
 
 theory L_axioms imports Formula Relative Reflection MetaExists begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/MetaExists.thy
--- a/src/ZF/Constructible/MetaExists.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/MetaExists.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header{*The meta-existential quantifier*}
+section{*The meta-existential quantifier*}
 
 theory MetaExists imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Normal.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Closed Unbounded Classes and Normal Functions*}
+section {*Closed Unbounded Classes and Normal Functions*}
 
 theory Normal imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Rank.thy
--- a/src/ZF/Constructible/Rank.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Rank.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Absoluteness for Order Types, Rank Functions and Well-Founded 
+section {*Absoluteness for Order Types, Rank Functions and Well-Founded 
          Relations*}
 
 theory Rank imports WF_absolute begin
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Rank_Separation.thy
--- a/src/ZF/Constructible/Rank_Separation.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Separation for Facts About Order Types, Rank Functions and 
+section {*Separation for Facts About Order Types, Rank Functions and 
       Well-Founded Relations*}
 
 theory Rank_Separation imports Rank Rec_Separation begin
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Separation for Facts About Recursion*}
+section {*Separation for Facts About Recursion*}
 
 theory Rec_Separation imports Separation Internalize begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Reflection.thy
--- a/src/ZF/Constructible/Reflection.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Reflection.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {* The Reflection Theorem*}
+section {* The Reflection Theorem*}
 
 theory Reflection imports Normal begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Relative.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Relativization and Absoluteness*}
+section {*Relativization and Absoluteness*}
 
 theory Relative imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Absoluteness for the Satisfies Relation on Formulas*}
+section {*Absoluteness for the Satisfies Relation on Formulas*}
 
 theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin 
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Separation.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header{*Early Instances of Separation and Strong Replacement*}
+section{*Early Instances of Separation and Strong Replacement*}
 
 theory Separation imports L_axioms WF_absolute begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/WF_absolute.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Absoluteness of Well-Founded Recursion*}
+section {*Absoluteness of Well-Founded Recursion*}
 
 theory WF_absolute imports WFrec begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/WFrec.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header{*Relativized Well-Founded Recursion*}
+section{*Relativized Well-Founded Recursion*}
 
 theory WFrec imports Wellorderings begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header {*Relativized Wellorderings*}
+section {*Relativized Wellorderings*}
 
 theory Wellorderings imports Relative begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Datatype_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1997  University of Cambridge
 *)
 
-header{*Datatype and CoDatatype Definitions*}
+section{*Datatype and CoDatatype Definitions*}
 
 theory Datatype_ZF
 imports Inductive_ZF Univ QUniv
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Epsilon.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-header{*Epsilon Induction and Recursion*}
+section{*Epsilon Induction and Recursion*}
 
 theory Epsilon imports Nat_ZF begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/EquivClass.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Equivalence Relations*}
+section{*Equivalence Relations*}
 
 theory EquivClass imports Trancl Perm begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Finite.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
 prove:  b \<in> Fin(A) ==> inj(b,b) \<subseteq> surj(b,b)
 *)
 
-header{*Finite Powerset Operator and Finite Function Space*}
+section{*Finite Powerset Operator and Finite Function Space*}
 
 theory Finite imports Inductive_ZF Epsilon Nat_ZF begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Fixedpt.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1992  University of Cambridge
 *)
 
-header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
+section{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
 
 theory Fixedpt imports equalities begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IMP/Com.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
-header {* Arithmetic expressions, boolean expressions, commands *}
+section {* Arithmetic expressions, boolean expressions, commands *}
 
 theory Com imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IMP/Denotation.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
-header {* Denotational semantics of expressions and commands *}
+section {* Denotational semantics of expressions and commands *}
 
 theory Denotation imports Com begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IMP/Equiv.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
-header {* Equivalence *}
+section {* Equivalence *}
 
 theory Equiv imports Denotation Com begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Acc.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* The accessible part of a relation *}
+section {* The accessible part of a relation *}
 
 theory Acc imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1992  University of Cambridge
 *)
 
-header {* Binary trees *}
+section {* Binary trees *}
 
 theory Binary_Trees imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Brouwer.thy
--- a/src/ZF/Induct/Brouwer.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Infinite branching datatype definitions *}
+section {* Infinite branching datatype definitions *}
 
 theory Brouwer imports Main_ZFC begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Comb.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Combinatory Logic example: the Church-Rosser Theorem *}
+section {* Combinatory Logic example: the Church-Rosser Theorem *}
 
 theory Comb imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Datatypes.thy
--- a/src/ZF/Induct/Datatypes.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Datatypes.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Sample datatype definitions *}
+section {* Sample datatype definitions *}
 
 theory Datatypes imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/ListN.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Lists of n elements *}
+section {* Lists of n elements *}
 
 theory ListN imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Mutil.thy
--- a/src/ZF/Induct/Mutil.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Mutil.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1996  University of Cambridge
 *)
 
-header {* The Mutilated Chess Board Problem, formalized inductively *}
+section {* The Mutilated Chess Board Problem, formalized inductively *}
 
 theory Mutil imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Ntree.thy
--- a/src/ZF/Induct/Ntree.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Ntree.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Datatype definition n-ary branching trees *}
+section {* Datatype definition n-ary branching trees *}
 
 theory Ntree imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Primrec.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Primitive Recursive Functions: the inductive definition *}
+section {* Primitive Recursive Functions: the inductive definition *}
 
 theory Primrec imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/PropLog.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-header {* Meta-theory of propositional logic *}
+section {* Meta-theory of propositional logic *}
 
 theory PropLog imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Rmap.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* An operator to ``map'' a relation over a list *}
+section {* An operator to ``map'' a relation over a list *}
 
 theory Rmap imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Term.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Terms over an alphabet *}
+section {* Terms over an alphabet *}
 
 theory Term imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Trees and forests, a mutually recursive type definition *}
+section {* Trees and forests, a mutually recursive type definition *}
 
 theory Tree_Forest imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
 Products are used only to derive "streamlined" induction rules for relations
 *)
 
-header{*Inductive and Coinductive Definitions*}
+section{*Inductive and Coinductive Definitions*}
 
 theory Inductive_ZF
 imports Fixedpt QPair Nat_ZF
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/InfDatatype.thy
--- a/src/ZF/InfDatatype.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/InfDatatype.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Infinite-Branching Datatype Definitions*}
+section{*Infinite-Branching Datatype Definitions*}
 
 theory InfDatatype imports Datatype_ZF Univ Finite Cardinal_AC begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/IntDiv_ZF.thy
--- a/src/ZF/IntDiv_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IntDiv_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -27,7 +27,7 @@
                           else        negateSnd (posDivAlg (~a,~b));
 *)
 
-header{*The Division Operators Div and Mod*}
+section{*The Division Operators Div and Mod*}
 
 theory IntDiv_ZF
 imports Bin OrderArith
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Int_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
+section{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
 
 theory Int_ZF imports EquivClass ArithSimp begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/List_ZF.thy
--- a/src/ZF/List_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/List_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Lists in Zermelo-Fraenkel Set Theory*}
+section{*Lists in Zermelo-Fraenkel Set Theory*}
 
 theory List_ZF imports Datatype_ZF ArithSimp begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Main_ZF.thy
--- a/src/ZF/Main_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Main_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -1,4 +1,4 @@
-header{*Theory Main: Everything Except AC*}
+section{*Theory Main: Everything Except AC*}
 
 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Nat_ZF.thy
--- a/src/ZF/Nat_ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Nat_ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*The Natural numbers As a Least Fixed Point*}
+section{*The Natural numbers As a Least Fixed Point*}
 
 theory Nat_ZF imports OrdQuant Bool begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/OrdQuant.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Authors:    Krzysztof Grabczewski and L C Paulson
 *)
 
-header {*Special quantifiers*}
+section {*Special quantifiers*}
 
 theory OrdQuant imports Ordinal begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Order.thy
--- a/src/ZF/Order.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Order.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -7,7 +7,7 @@
 Additional definitions and lemmas for reflexive orders.
 *)
 
-header{*Partial and Total Orderings: Basic Definitions and Properties*}
+section{*Partial and Total Orderings: Basic Definitions and Properties*}
 
 theory Order imports WF Perm begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/OrderArith.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
+section{*Combining Orderings: Foundations of Ordinal Arithmetic*}
 
 theory OrderArith imports Order Sum Ordinal begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/OrderType.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Order Types and Ordinal Arithmetic*}
+section{*Order Types and Ordinal Arithmetic*}
 
 theory OrderType imports OrderArith OrdQuant Nat_ZF begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Ordinal.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Transitive Sets and Ordinals*}
+section{*Transitive Sets and Ordinals*}
 
 theory Ordinal imports WF Bool equalities begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Perm.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -8,7 +8,7 @@
   -- Lemmas for the Schroeder-Bernstein Theorem
 *)
 
-header{*Injections, Surjections, Bijections, Composition*}
+section{*Injections, Surjections, Bijections, Composition*}
 
 theory Perm imports func begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/QPair.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -8,7 +8,7 @@
 is not a limit ordinal?
 *)
 
-header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
+section{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
 
 theory QPair imports Sum func begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/QUniv.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-header{*A Small Universe for Lazy Recursive Types*}
+section{*A Small Universe for Lazy Recursive Types*}
 
 theory QUniv imports Univ QPair begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Sum.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-header{*Disjoint Sums*}
+section{*Disjoint Sums*}
 
 theory Sum imports Bool equalities begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Trancl.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1992  University of Cambridge
 *)
 
-header{*Relations: Their General Properties and Transitive Closure*}
+section{*Relations: Their General Properties and Transitive Closure*}
 
 theory Trancl imports Fixedpt Perm begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/AllocBase.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2001  University of Cambridge
 *)
 
-header{*Common declarations for Chandy and Charpentier's Allocator*}
+section{*Common declarations for Chandy and Charpentier's Allocator*}
 
 theory AllocBase imports Follows MultisetSum Guar begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Comp.thy
--- a/src/ZF/UNITY/Comp.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Comp.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -13,7 +13,7 @@
   
 *)
 
-header{*Composition*}
+section{*Composition*}
 
 theory Comp imports Union Increasing begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2001  University of Cambridge
 *)
 
-header{*Weak Safety Properties*}
+section{*Weak Safety Properties*}
 
 theory Constrains
 imports UNITY
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/FP.thy
--- a/src/ZF/UNITY/FP.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/FP.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -7,7 +7,7 @@
 Theory ported from HOL.
 *)
 
-header{*Fixed Point of a Program*}
+section{*Fixed Point of a Program*}
 
 theory FP imports UNITY begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Follows.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
 Theory ported from HOL.
 *)
 
-header{*The "Follows" relation of Charpentier and Sivilotte*}
+section{*The "Follows" relation of Charpentier and Sivilotte*}
 
 theory Follows imports SubstAx Increasing begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
 Based on Lex/Prefix
 *)
 
-header{*Charpentier's Generalized Prefix Relation*}
+section{*Charpentier's Generalized Prefix Relation*}
 
 theory GenPrefix
 imports Main
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Guar.thy
--- a/src/ZF/UNITY/Guar.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Guar.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -19,7 +19,7 @@
 *)
 
 
-header{*The Chandy-Sanders Guarantees Operator*}
+section{*The Chandy-Sanders Guarantees Operator*}
 
 theory Guar imports Comp begin 
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Increasing.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -6,7 +6,7 @@
 relation r over the domain A. 
 *)
 
-header{*Charpentier's "Increasing" Relation*}
+section{*Charpentier's "Increasing" Relation*}
 
 theory Increasing imports Constrains Monotonicity begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Monotonicity.thy
--- a/src/ZF/UNITY/Monotonicity.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -6,7 +6,7 @@
 set relations.
 *)
 
-header{*Monotonicity of an Operator WRT a Relation*}
+section{*Monotonicity of an Operator WRT a Relation*}
 
 theory Monotonicity imports GenPrefix MultisetSum
 begin
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/MultisetSum.thy
--- a/src/ZF/UNITY/MultisetSum.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/MultisetSum.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Sidi O Ehmety
 *)
 
-header {*Setsum for Multisets*}
+section {*Setsum for Multisets*}
 
 theory MultisetSum
 imports "../Induct/Multiset"
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Mutex.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
 reduce to the empty set.
 *)
 
-header{*Mutual Exclusion*}
+section{*Mutual Exclusion*}
 
 theory Mutex
 imports SubstAx
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/State.thy
--- a/src/ZF/UNITY/State.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/State.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -8,7 +8,7 @@
  - variables can be quantified over.
 *)
 
-header{*UNITY Program States*}
+section{*UNITY Program States*}
 
 theory State imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
 Theory ported from HOL.
 *)
 
-header{*Weak LeadsTo relation (restricted to the set of reachable states)*}
+section{*Weak LeadsTo relation (restricted to the set of reachable states)*}
 
 theory SubstAx
 imports WFair Constrains
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/UNITY.thy
--- a/src/ZF/UNITY/UNITY.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/UNITY.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2001  University of Cambridge
 *)
 
-header {*The Basic UNITY Theory*}
+section {*The Basic UNITY Theory*}
 
 theory UNITY imports State begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/UNITY/WFair.thy
--- a/src/ZF/UNITY/WFair.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/WFair.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1998  University of Cambridge
 *)
 
-header{*Progress under Weak Fairness*}
+section{*Progress under Weak Fairness*}
 
 theory WFair
 imports UNITY Main_ZFC
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Univ.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
   But Ind_Syntax.univ refers to the constant "Univ.univ"
 *)
 
-header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
+section{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
 
 theory Univ imports Epsilon Cardinal begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/WF.thy
--- a/src/ZF/WF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/WF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -14,7 +14,7 @@
 a mess.
 *)
 
-header{*Well-Founded Recursion*}
+section{*Well-Founded Recursion*}
 
 theory WF imports Trancl begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ZF.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-header{*Zermelo-Fraenkel Set Theory*}
+section{*Zermelo-Fraenkel Set Theory*}
 
 theory ZF
 imports "~~/src/FOL/FOL"
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Zorn.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header{*Zorn's Lemma*}
+section{*Zorn's Lemma*}
 
 theory Zorn imports OrderArith AC Inductive_ZF begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/document/root.tex
--- a/src/ZF/document/root.tex	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/document/root.tex	Sun Nov 02 16:39:54 2014 +0100
@@ -25,8 +25,7 @@
 
 \newpage
 
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
 
 \parindent 0pt\parskip 0.5ex
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/equalities.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1992  University of Cambridge
 *)
 
-header{*Basic Equalities and Inclusions*}
+section{*Basic Equalities and Inclusions*}
 
 theory equalities imports pair begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/CoUnit.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-header {* Trivial codatatype definitions, one of which goes wrong! *}
+section {* Trivial codatatype definitions, one of which goes wrong! *}
 
 theory CoUnit imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/Group.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -1,6 +1,6 @@
 (*  Title:      ZF/ex/Group.thy *)
 
-header {* Groups *}
+section {* Groups *}
 
 theory Group imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ex/Primes.thy
--- a/src/ZF/ex/Primes.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/Primes.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1996  University of Cambridge
 *)
 
-header{*The Divides Relation and Euclid's algorithm for the GCD*}
+section{*The Divides Relation and Euclid's algorithm for the GCD*}
 
 theory Primes imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/Ring.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
 
 *)
 
-header {* Rings *}
+section {* Rings *}
 
 theory Ring imports Group begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/ex/misc.thy
--- a/src/ZF/ex/misc.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/misc.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
 Composition of homomorphisms, Pastre's examples, ...
 *)
 
-header{*Miscellaneous ZF Examples*}
+section{*Miscellaneous ZF Examples*}
 
 theory misc imports Main begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/func.thy
--- a/src/ZF/func.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/func.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1991  University of Cambridge
 *)
 
-header{*Functions, Function Spaces, Lambda-Abstraction*}
+section{*Functions, Function Spaces, Lambda-Abstraction*}
 
 theory func imports equalities Sum begin
 
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/pair.thy
--- a/src/ZF/pair.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/pair.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1992  University of Cambridge
 *)
 
-header{*Ordered Pairs*}
+section{*Ordered Pairs*}
 
 theory pair imports upair
 begin
diff -r e2c0d8ef29cb -r c399ae4b836f src/ZF/upair.thy
--- a/src/ZF/upair.thy	Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/upair.thy	Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
     Ordered pairs and descriptions are defined using cons ("set notation")
 *)
 
-header{*Unordered Pairs*}
+section{*Unordered Pairs*}
 
 theory upair
 imports ZF