# HG changeset patch
# User wenzelm
# Date 1414944961 -3600
# Node ID 0baae4311a9f715a72050052bf4ec2a96276b5b4
# Parent  143c85e3cdb52992505e6dfd8ce919b6d0488763
modernized header;

diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Adm.thy
--- a/src/HOL/HOLCF/Adm.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Adm.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger and Brian Huffman
 *)
 
-header {* Admissibility and compactness *}
+section {* Admissibility and compactness *}
 
 theory Adm
 imports Cont
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Algebraic deflations *}
+section {* Algebraic deflations *}
 
 theory Algebraic
 imports Universal Map_Functions
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Profinite and bifinite cpos *}
+section {* Profinite and bifinite cpos *}
 
 theory Bifinite
 imports Map_Functions "~~/src/HOL/Library/Countable"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The type of continuous functions *}
+section {* The type of continuous functions *}
 
 theory Cfun
 imports Cpodef Fun_Cpo Product_Cpo
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* A compact basis for powerdomains *}
+section {* A compact basis for powerdomains *}
 
 theory Compact_Basis
 imports Universal
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Defining algebraic domains by ideal completion *}
+section {* Defining algebraic domains by ideal completion *}
 
 theory Completion
 imports Plain_HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Cont.thy
--- a/src/HOL/HOLCF/Cont.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Cont.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Continuity and monotonicity *}
+section {* Continuity and monotonicity *}
 
 theory Cont
 imports Pcpo
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Convex powerdomain *}
+section {* Convex powerdomain *}
 
 theory ConvexPD
 imports UpperPD LowerPD
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Subtypes of pcpos *}
+section {* Subtypes of pcpos *}
 
 theory Cpodef
 imports Adm
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Cprod.thy
--- a/src/HOL/HOLCF/Cprod.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Cprod.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-header {* The cpo of cartesian products *}
+section {* The cpo of cartesian products *}
 
 theory Cprod
 imports Cfun
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Deflation.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Continuous deflations and ep-pairs *}
+section {* Continuous deflations and ep-pairs *}
 
 theory Deflation
 imports Plain_HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Discrete.thy
--- a/src/HOL/HOLCF/Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow
 *)
 
-header {* Discrete cpo types *}
+section {* Discrete cpo types *}
 
 theory Discrete
 imports Cont
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Domain package *}
+section {* Domain package *}
 
 theory Domain
 imports Representable Domain_Aux
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Domain package support *}
+section {* Domain package support *}
 
 theory Domain_Aux
 imports Map_Functions Fixrec
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
+section {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
 
 theory Buffer_adm
 imports Buffer Stream_adm
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/FOCUS/FOCUS.thy
--- a/src/HOL/HOLCF/FOCUS/FOCUS.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/FOCUS.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-header {* Top level of FOCUS *}
+section {* Top level of FOCUS *}
 
 theory FOCUS
 imports Fstream
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -6,7 +6,7 @@
 TODO: integrate Fstreams.thy
 *)
 
-header {* FOCUS flat streams *}
+section {* FOCUS flat streams *}
 
 theory Fstream
 imports "~~/src/HOL/HOLCF/Library/Stream"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-header {* Admissibility for streams *}
+section {* Admissibility for streams *}
 
 theory Stream_adm
 imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Fix.thy
--- a/src/HOL/HOLCF/Fix.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Fix.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Fixed point operator and admissibility *}
+section {* Fixed point operator and admissibility *}
 
 theory Fix
 imports Cfun
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Amber Telfer and Brian Huffman
 *)
 
-header "Package for defining recursive functions in HOLCF"
+section "Package for defining recursive functions in HOLCF"
 
 theory Fixrec
 imports Plain_HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Fun_Cpo.thy
--- a/src/HOL/HOLCF/Fun_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Fun_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Class instances for the full function space *}
+section {* Class instances for the full function space *}
 
 theory Fun_Cpo
 imports Adm
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IMP/Denotational.thy
--- a/src/HOL/HOLCF/IMP/Denotational.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1996 TUM
 *)
 
-header "Denotational Semantics of Commands in HOLCF"
+section "Denotational Semantics of Commands in HOLCF"
 
 theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
 
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1997 TUM
 *)
 
-header "Correctness of Hoare by Fixpoint Reasoning"
+section "Correctness of Hoare by Fixpoint Reasoning"
 
 theory HoareEx imports Denotational begin
 
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The transmission channel *}
+section {* The transmission channel *}
 
 theory Abschannel
 imports IOA Action Lemmas
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The transmission channel -- finite version *}
+section {* The transmission channel -- finite version *}
 
 theory Abschannel_finite
 imports Abschannel IOA Action Lemmas
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Action.thy
--- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The set of all actions of the system *}
+section {* The set of all actions of the system *}
 
 theory Action
 imports Packet
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The main correctness proof: System_fin implements System *}
+section {* The main correctness proof: System_fin implements System *}
 
 theory Correctness
 imports IOA Env Impl Impl_finite
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Env.thy
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The environment *}
+section {* The environment *}
 
 theory Env
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Impl.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The implementation *}
+section {* The implementation *}
 
 theory Impl
 imports Sender Receiver Abschannel
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The implementation *}
+section {* The implementation *}
 
 theory Impl_finite
 imports Sender Receiver Abschannel_finite
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Packet.thy
--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Packets *}
+section {* Packets *}
 
 theory Packet
 imports Main
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The implementation: receiver *}
+section {* The implementation: receiver *}
 
 theory Receiver
 imports IOA Action Lemmas
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The implementation: sender *}
+section {* The implementation: sender *}
 
 theory Sender
 imports IOA Action Lemmas
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ABP/Spec.thy
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The specification of reliable transmission *}
+section {* The specification of reliable transmission *}
 
 theory Spec
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The (faulty) transmission channel (both directions) *}
+section {* The (faulty) transmission channel (both directions) *}
 
 theory Abschannel
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Action.thy
--- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* The set of all actions of the system *}
+section {* The set of all actions of the system *}
 
 theory Action
 imports Packet
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* The main correctness proof: Impl implements Spec *}
+section {* The main correctness proof: Impl implements Spec *}
 
 theory Correctness
 imports Impl Spec
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* The implementation *}
+section {* The implementation *}
 
 theory Impl
 imports Sender Receiver Abschannel
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* Axiomatic multisets *}
+section {* Axiomatic multisets *}
 
 theory Multiset
 imports Lemmas
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* The implementation: receiver *}
+section {* The implementation: receiver *}
 
 theory Receiver
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* The implementation: sender *}
+section {* The implementation: sender *}
 
 theory Sender
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/NTP/Spec.thy
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-header {* The specification of reliable transmission *}
+section {* The specification of reliable transmission *}
 
 theory Spec
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/Storage/Action.thy
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The set of all actions of the system *}
+section {* The set of all actions of the system *}
 
 theory Action
 imports Main
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Correctness Proof *}
+section {* Correctness Proof *}
 
 theory Correctness
 imports SimCorrectness Spec Impl
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/Storage/Impl.thy
--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The implementation of a memory *}
+section {* The implementation of a memory *}
 
 theory Impl
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/Storage/Spec.thy
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The specification of a memory *}
+section {* The specification of a memory *}
 
 theory Spec
 imports IOA Action
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Trivial Abstraction Example *}
+section {* Trivial Abstraction Example *}
 
 theory TrivEx
 imports Abstraction
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Trivial Abstraction Example with fairness *}
+section {* Trivial Abstraction Example with fairness *}
 
 theory TrivEx2
 imports IOA Abstraction
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Abstraction Theory -- tailored for I/O automata *}
+section {* Abstraction Theory -- tailored for I/O automata *}
 
 theory Abstraction
 imports LiveIOA
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Asig.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
 *)
 
-header {* Action signatures *}
+section {* Action signatures *}
 
 theory Asig
 imports Main
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
 *)
 
-header {* The I/O automata of Lynch and Tuttle in HOLCF *}
+section {* The I/O automata of Lynch and Tuttle in HOLCF *}
 
 theory Automata
 imports Asig
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Compositionality on Execution level *}
+section {* Compositionality on Execution level *}
 
 theory CompoExecs
 imports Traces
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Compositionality on Schedule level *}
+section {* Compositionality on Schedule level *}
 
 theory CompoScheds
 imports CompoExecs
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *) 
 
-header {* Compositionality on Trace level *}
+section {* Compositionality on Trace level *}
 
 theory CompoTraces
 imports CompoScheds ShortExecutions
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Compositionality of I/O automata *}
+section {* Compositionality of I/O automata *}
 theory Compositionality
 imports CompoTraces
 begin
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Deadlock freedom of I/O Automata *}
+section {* Deadlock freedom of I/O Automata *}
 
 theory Deadlock
 imports RefCorrectness CompoScheds
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/IOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* The theory of I/O automata in HOLCF *}
+section {* The theory of I/O automata in HOLCF *}
 
 theory IOA
 imports SimCorrectness Compositionality Deadlock
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Live I/O automata -- specified by temproal formulas *}
+section {* Live I/O automata -- specified by temproal formulas *}
 
 theory LiveIOA
 imports TLS
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Logical Connectives lifted to predicates *}
+section {* Logical Connectives lifted to predicates *}
 
 theory Pred
 imports Main
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Correctness of Refinement Mappings in HOLCF/IOA *}
+section {* Correctness of Refinement Mappings in HOLCF/IOA *}
 
 theory RefCorrectness
 imports RefMappings
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Refinement Mappings in HOLCF/IOA *}
+section {* Refinement Mappings in HOLCF/IOA *}
 
 theory RefMappings
 imports Traces
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
+section {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
 
 theory Seq
 imports "../../HOLCF"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Correctness of Simulations in HOLCF/IOA *}
+section {* Correctness of Simulations in HOLCF/IOA *}
 
 theory SimCorrectness
 imports Simulations
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Simulations in HOLCF/IOA *}
+section {* Simulations in HOLCF/IOA *}
 
 theory Simulations
 imports RefCorrectness
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* A General Temporal Logic *}
+section {* A General Temporal Logic *}
 
 theory TL
 imports Pred Sequence
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Temporal Logic of Steps -- tailored for I/O automata *}
+section {* Temporal Logic of Steps -- tailored for I/O automata *}
 
 theory TLS
 imports IOA TL
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-header {* Executions and Traces of I/O automata in HOLCF *}
+section {* Executions and Traces of I/O automata in HOLCF *}
 
 theory Traces
 imports Sequence Automata
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Bool_Discrete.thy
--- a/src/HOL/HOLCF/Library/Bool_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Discrete cpo instance for booleans *}
+section {* Discrete cpo instance for booleans *}
 
 theory Bool_Discrete
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Char_Discrete.thy
--- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Discrete cpo instance for 8-bit char type *}
+section {* Discrete cpo instance for 8-bit char type *}
 
 theory Char_Discrete
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Algebraic deflations are a bifinite domain *}
+section {* Algebraic deflations are a bifinite domain *}
 
 theory Defl_Bifinite
 imports HOLCF "~~/src/HOL/Library/Infinite_Set"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/HOL_Cpo.thy
--- a/src/HOL/HOLCF/Library/HOL_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Cpo class instances for all HOL types *}
+section {* Cpo class instances for all HOL types *}
 
 theory HOL_Cpo
 imports
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Int_Discrete.thy
--- a/src/HOL/HOLCF/Library/Int_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Discrete cpo instance for integers *}
+section {* Discrete cpo instance for integers *}
 
 theory Int_Discrete
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Lists as a complete partial order *}
+section {* Lists as a complete partial order *}
 
 theory List_Cpo
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/List_Predomain.thy
--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Predomain class instance for HOL list type *}
+section {* Predomain class instance for HOL list type *}
 
 theory List_Predomain
 imports List_Cpo Sum_Cpo
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Nat_Discrete.thy
--- a/src/HOL/HOLCF/Library/Nat_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Discrete cpo instance for naturals *}
+section {* Discrete cpo instance for naturals *}
 
 theory Nat_Discrete
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Option_Cpo.thy
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Cpo class instance for HOL option type *}
+section {* Cpo class instance for HOL option type *}
 
 theory Option_Cpo
 imports HOLCF Sum_Cpo
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Stream.thy
--- a/src/HOL/HOLCF/Library/Stream.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Stream.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
 *)
 
-header {* General Stream domain *}
+section {* General Stream domain *}
 
 theory Stream
 imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The cpo of disjoint sums *}
+section {* The cpo of disjoint sums *}
 
 theory Sum_Cpo
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Mueller
 *)
 
-header {* Lifting types of class type to flat pcpo's *}
+section {* Lifting types of class type to flat pcpo's *}
 
 theory Lift
 imports Discrete Up
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Lower powerdomain *}
+section {* Lower powerdomain *}
 
 theory LowerPD
 imports Compact_Basis
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Map_Functions.thy
--- a/src/HOL/HOLCF/Map_Functions.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Map functions for various types *}
+section {* Map functions for various types *}
 
 theory Map_Functions
 imports Deflation
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/One.thy
--- a/src/HOL/HOLCF/One.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/One.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Oscar Slotosch
 *)
 
-header {* The unit domain *}
+section {* The unit domain *}
 
 theory One
 imports Lift
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-header {* Classes cpo and pcpo *}
+section {* Classes cpo and pcpo *}
 
 theory Pcpo
 imports Porder
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Plain_HOLCF.thy
--- a/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Plain HOLCF *}
+section {* Plain HOLCF *}
 
 theory Plain_HOLCF
 imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Porder.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger and Brian Huffman
 *)
 
-header {* Partial orders *}
+section {* Partial orders *}
 
 theory Porder
 imports Main
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Powerdomains.thy
--- a/src/HOL/HOLCF/Powerdomains.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Powerdomains *}
+section {* Powerdomains *}
 
 theory Powerdomains
 imports ConvexPD Domain
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Product_Cpo.thy
--- a/src/HOL/HOLCF/Product_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Product_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-header {* The cpo of cartesian products *}
+section {* The cpo of cartesian products *}
 
 theory Product_Cpo
 imports Adm
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Representable.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Representable domains *}
+section {* Representable domains *}
 
 theory Representable
 imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Sfun.thy
--- a/src/HOL/HOLCF/Sfun.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The Strict Function Type *}
+section {* The Strict Function Type *}
 
 theory Sfun
 imports Cfun
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Sprod.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The type of strict products *}
+section {* The type of strict products *}
 
 theory Sprod
 imports Cfun
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Ssum.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The type of strict sums *}
+section {* The type of strict sums *}
 
 theory Ssum
 imports Tr
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Tr.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-header {* The type of lifted booleans *}
+section {* The type of lifted booleans *}
 
 theory Tr
 imports Lift
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Tutorial/Domain_ex.thy
--- a/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Domain package examples *}
+section {* Domain package examples *}
 
 theory Domain_ex
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Tutorial/Fixrec_ex.thy
--- a/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Fixrec package examples *}
+section {* Fixrec package examples *}
 
 theory Fixrec_ex
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Tutorial/New_Domain.thy
--- a/src/HOL/HOLCF/Tutorial/New_Domain.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Definitional domain package *}
+section {* Definitional domain package *}
 
 theory New_Domain
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* A universal bifinite domain *}
+section {* A universal bifinite domain *}
 
 theory Universal
 imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/Up.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-header {* The type of lifted values *}
+section {* The type of lifted values *}
 
 theory Up
 imports Cfun
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Upper powerdomain *}
+section {* Upper powerdomain *}
 
 theory UpperPD
 imports Compact_Basis
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/document/root.tex
--- a/src/HOL/HOLCF/document/root.tex	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/document/root.tex	Sun Nov 02 17:16:01 2014 +0100
@@ -27,8 +27,7 @@
 
 \newpage
 
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
 
 \parindent 0pt\parskip 0.5ex
 \input{session}
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Internal domain package proofs done manually *}
+section {* Internal domain package proofs done manually *}
 
 theory Domain_Proofs
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Recursive let bindings *}
+section {* Recursive let bindings *}
 
 theory Letrec
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/ex/Loop.thy
--- a/src/HOL/HOLCF/ex/Loop.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Loop.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-header {* Theory for a loop primitive like while *}
+section {* Theory for a loop primitive like while *}
 
 theory Loop
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* An experimental pattern-matching notation *}
+section {* An experimental pattern-matching notation *}
 
 theory Pattern_Match
 imports HOLCF
diff -r 143c85e3cdb5 -r 0baae4311a9f src/HOL/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Sun Nov 02 17:14:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Sun Nov 02 17:16:01 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Powerdomain examples *}
+section {* Powerdomain examples *}
 
 theory Powerdomain_ex
 imports HOLCF