modernized header;
authorwenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 588800baae4311a9f
parent 58879 143c85e3cdb5
child 58881 b9556a055632
modernized header;
src/HOL/HOLCF/Adm.thy
src/HOL/HOLCF/Algebraic.thy
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Compact_Basis.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/Cont.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Cprod.thy
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Discrete.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
src/HOL/HOLCF/FOCUS/FOCUS.thy
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/Fix.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/Fun_Cpo.thy
src/HOL/HOLCF/IMP/Denotational.thy
src/HOL/HOLCF/IMP/HoareEx.thy
src/HOL/HOLCF/IOA/ABP/Abschannel.thy
src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOL/HOLCF/IOA/ABP/Action.thy
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/HOLCF/IOA/ABP/Env.thy
src/HOL/HOLCF/IOA/ABP/Impl.thy
src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
src/HOL/HOLCF/IOA/ABP/Packet.thy
src/HOL/HOLCF/IOA/ABP/Receiver.thy
src/HOL/HOLCF/IOA/ABP/Sender.thy
src/HOL/HOLCF/IOA/ABP/Spec.thy
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
src/HOL/HOLCF/IOA/NTP/Action.thy
src/HOL/HOLCF/IOA/NTP/Correctness.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/HOLCF/IOA/NTP/Multiset.thy
src/HOL/HOLCF/IOA/NTP/Receiver.thy
src/HOL/HOLCF/IOA/NTP/Sender.thy
src/HOL/HOLCF/IOA/NTP/Spec.thy
src/HOL/HOLCF/IOA/Storage/Action.thy
src/HOL/HOLCF/IOA/Storage/Correctness.thy
src/HOL/HOLCF/IOA/Storage/Impl.thy
src/HOL/HOLCF/IOA/Storage/Spec.thy
src/HOL/HOLCF/IOA/ex/TrivEx.thy
src/HOL/HOLCF/IOA/ex/TrivEx2.thy
src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOL/HOLCF/IOA/meta_theory/Asig.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOL/HOLCF/IOA/meta_theory/IOA.thy
src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOL/HOLCF/IOA/meta_theory/Pred.thy
src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOL/HOLCF/IOA/meta_theory/Seq.thy
src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
src/HOL/HOLCF/IOA/meta_theory/TL.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/HOLCF/Library/Bool_Discrete.thy
src/HOL/HOLCF/Library/Char_Discrete.thy
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/Library/HOL_Cpo.thy
src/HOL/HOLCF/Library/Int_Discrete.thy
src/HOL/HOLCF/Library/List_Cpo.thy
src/HOL/HOLCF/Library/List_Predomain.thy
src/HOL/HOLCF/Library/Nat_Discrete.thy
src/HOL/HOLCF/Library/Option_Cpo.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/HOLCF/Library/Sum_Cpo.thy
src/HOL/HOLCF/Lift.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Map_Functions.thy
src/HOL/HOLCF/One.thy
src/HOL/HOLCF/Pcpo.thy
src/HOL/HOLCF/Plain_HOLCF.thy
src/HOL/HOLCF/Porder.thy
src/HOL/HOLCF/Powerdomains.thy
src/HOL/HOLCF/Product_Cpo.thy
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/Sfun.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/HOLCF/Tr.thy
src/HOL/HOLCF/Tutorial/Domain_ex.thy
src/HOL/HOLCF/Tutorial/Fixrec_ex.thy
src/HOL/HOLCF/Tutorial/New_Domain.thy
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/Up.thy
src/HOL/HOLCF/UpperPD.thy
src/HOL/HOLCF/document/root.tex
src/HOL/HOLCF/ex/Domain_Proofs.thy
src/HOL/HOLCF/ex/Letrec.thy
src/HOL/HOLCF/ex/Loop.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/HOLCF/ex/Powerdomain_ex.thy
     1.1 --- a/src/HOL/HOLCF/Adm.thy	Sun Nov 02 17:14:15 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Adm.thy	Sun Nov 02 17:16:01 2014 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Franz Regensburger and Brian Huffman
     1.5  *)
     1.6  
     1.7 -header {* Admissibility and compactness *}
     1.8 +section {* Admissibility and compactness *}
     1.9  
    1.10  theory Adm
    1.11  imports Cont
     2.1 --- a/src/HOL/HOLCF/Algebraic.thy	Sun Nov 02 17:14:15 2014 +0100
     2.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Sun Nov 02 17:16:01 2014 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Brian Huffman
     2.5  *)
     2.6  
     2.7 -header {* Algebraic deflations *}
     2.8 +section {* Algebraic deflations *}
     2.9  
    2.10  theory Algebraic
    2.11  imports Universal Map_Functions
     3.1 --- a/src/HOL/HOLCF/Bifinite.thy	Sun Nov 02 17:14:15 2014 +0100
     3.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Sun Nov 02 17:16:01 2014 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Brian Huffman
     3.5  *)
     3.6  
     3.7 -header {* Profinite and bifinite cpos *}
     3.8 +section {* Profinite and bifinite cpos *}
     3.9  
    3.10  theory Bifinite
    3.11  imports Map_Functions "~~/src/HOL/Library/Countable"
     4.1 --- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 02 17:14:15 2014 +0100
     4.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 02 17:16:01 2014 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Brian Huffman
     4.5  *)
     4.6  
     4.7 -header {* The type of continuous functions *}
     4.8 +section {* The type of continuous functions *}
     4.9  
    4.10  theory Cfun
    4.11  imports Cpodef Fun_Cpo Product_Cpo
     5.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Sun Nov 02 17:14:15 2014 +0100
     5.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Sun Nov 02 17:16:01 2014 +0100
     5.3 @@ -2,7 +2,7 @@
     5.4      Author:     Brian Huffman
     5.5  *)
     5.6  
     5.7 -header {* A compact basis for powerdomains *}
     5.8 +section {* A compact basis for powerdomains *}
     5.9  
    5.10  theory Compact_Basis
    5.11  imports Universal
     6.1 --- a/src/HOL/HOLCF/Completion.thy	Sun Nov 02 17:14:15 2014 +0100
     6.2 +++ b/src/HOL/HOLCF/Completion.thy	Sun Nov 02 17:16:01 2014 +0100
     6.3 @@ -2,7 +2,7 @@
     6.4      Author:     Brian Huffman
     6.5  *)
     6.6  
     6.7 -header {* Defining algebraic domains by ideal completion *}
     6.8 +section {* Defining algebraic domains by ideal completion *}
     6.9  
    6.10  theory Completion
    6.11  imports Plain_HOLCF
     7.1 --- a/src/HOL/HOLCF/Cont.thy	Sun Nov 02 17:14:15 2014 +0100
     7.2 +++ b/src/HOL/HOLCF/Cont.thy	Sun Nov 02 17:16:01 2014 +0100
     7.3 @@ -3,7 +3,7 @@
     7.4      Author:     Brian Huffman
     7.5  *)
     7.6  
     7.7 -header {* Continuity and monotonicity *}
     7.8 +section {* Continuity and monotonicity *}
     7.9  
    7.10  theory Cont
    7.11  imports Pcpo
     8.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Nov 02 17:14:15 2014 +0100
     8.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Nov 02 17:16:01 2014 +0100
     8.3 @@ -2,7 +2,7 @@
     8.4      Author:     Brian Huffman
     8.5  *)
     8.6  
     8.7 -header {* Convex powerdomain *}
     8.8 +section {* Convex powerdomain *}
     8.9  
    8.10  theory ConvexPD
    8.11  imports UpperPD LowerPD
     9.1 --- a/src/HOL/HOLCF/Cpodef.thy	Sun Nov 02 17:14:15 2014 +0100
     9.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Sun Nov 02 17:16:01 2014 +0100
     9.3 @@ -2,7 +2,7 @@
     9.4      Author:     Brian Huffman
     9.5  *)
     9.6  
     9.7 -header {* Subtypes of pcpos *}
     9.8 +section {* Subtypes of pcpos *}
     9.9  
    9.10  theory Cpodef
    9.11  imports Adm
    10.1 --- a/src/HOL/HOLCF/Cprod.thy	Sun Nov 02 17:14:15 2014 +0100
    10.2 +++ b/src/HOL/HOLCF/Cprod.thy	Sun Nov 02 17:16:01 2014 +0100
    10.3 @@ -2,7 +2,7 @@
    10.4      Author:     Franz Regensburger
    10.5  *)
    10.6  
    10.7 -header {* The cpo of cartesian products *}
    10.8 +section {* The cpo of cartesian products *}
    10.9  
   10.10  theory Cprod
   10.11  imports Cfun
    11.1 --- a/src/HOL/HOLCF/Deflation.thy	Sun Nov 02 17:14:15 2014 +0100
    11.2 +++ b/src/HOL/HOLCF/Deflation.thy	Sun Nov 02 17:16:01 2014 +0100
    11.3 @@ -2,7 +2,7 @@
    11.4      Author:     Brian Huffman
    11.5  *)
    11.6  
    11.7 -header {* Continuous deflations and ep-pairs *}
    11.8 +section {* Continuous deflations and ep-pairs *}
    11.9  
   11.10  theory Deflation
   11.11  imports Plain_HOLCF
    12.1 --- a/src/HOL/HOLCF/Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
    12.2 +++ b/src/HOL/HOLCF/Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
    12.3 @@ -2,7 +2,7 @@
    12.4      Author:     Tobias Nipkow
    12.5  *)
    12.6  
    12.7 -header {* Discrete cpo types *}
    12.8 +section {* Discrete cpo types *}
    12.9  
   12.10  theory Discrete
   12.11  imports Cont
    13.1 --- a/src/HOL/HOLCF/Domain.thy	Sun Nov 02 17:14:15 2014 +0100
    13.2 +++ b/src/HOL/HOLCF/Domain.thy	Sun Nov 02 17:16:01 2014 +0100
    13.3 @@ -2,7 +2,7 @@
    13.4      Author:     Brian Huffman
    13.5  *)
    13.6  
    13.7 -header {* Domain package *}
    13.8 +section {* Domain package *}
    13.9  
   13.10  theory Domain
   13.11  imports Representable Domain_Aux
    14.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Sun Nov 02 17:14:15 2014 +0100
    14.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Sun Nov 02 17:16:01 2014 +0100
    14.3 @@ -2,7 +2,7 @@
    14.4      Author:     Brian Huffman
    14.5  *)
    14.6  
    14.7 -header {* Domain package support *}
    14.8 +section {* Domain package support *}
    14.9  
   14.10  theory Domain_Aux
   14.11  imports Map_Functions Fixrec
    15.1 --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 02 17:14:15 2014 +0100
    15.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 02 17:16:01 2014 +0100
    15.3 @@ -2,7 +2,7 @@
    15.4      Author:     David von Oheimb, TU Muenchen
    15.5  *)
    15.6  
    15.7 -header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
    15.8 +section {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
    15.9  
   15.10  theory Buffer_adm
   15.11  imports Buffer Stream_adm
    16.1 --- a/src/HOL/HOLCF/FOCUS/FOCUS.thy	Sun Nov 02 17:14:15 2014 +0100
    16.2 +++ b/src/HOL/HOLCF/FOCUS/FOCUS.thy	Sun Nov 02 17:16:01 2014 +0100
    16.3 @@ -2,7 +2,7 @@
    16.4      Author:     David von Oheimb, TU Muenchen
    16.5  *)
    16.6  
    16.7 -header {* Top level of FOCUS *}
    16.8 +section {* Top level of FOCUS *}
    16.9  
   16.10  theory FOCUS
   16.11  imports Fstream
    17.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Sun Nov 02 17:14:15 2014 +0100
    17.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Sun Nov 02 17:16:01 2014 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4  TODO: integrate Fstreams.thy
    17.5  *)
    17.6  
    17.7 -header {* FOCUS flat streams *}
    17.8 +section {* FOCUS flat streams *}
    17.9  
   17.10  theory Fstream
   17.11  imports "~~/src/HOL/HOLCF/Library/Stream"
    18.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Sun Nov 02 17:14:15 2014 +0100
    18.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Sun Nov 02 17:16:01 2014 +0100
    18.3 @@ -2,7 +2,7 @@
    18.4      Author:     David von Oheimb, TU Muenchen
    18.5  *)
    18.6  
    18.7 -header {* Admissibility for streams *}
    18.8 +section {* Admissibility for streams *}
    18.9  
   18.10  theory Stream_adm
   18.11  imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
    19.1 --- a/src/HOL/HOLCF/Fix.thy	Sun Nov 02 17:14:15 2014 +0100
    19.2 +++ b/src/HOL/HOLCF/Fix.thy	Sun Nov 02 17:16:01 2014 +0100
    19.3 @@ -3,7 +3,7 @@
    19.4      Author:     Brian Huffman
    19.5  *)
    19.6  
    19.7 -header {* Fixed point operator and admissibility *}
    19.8 +section {* Fixed point operator and admissibility *}
    19.9  
   19.10  theory Fix
   19.11  imports Cfun
    20.1 --- a/src/HOL/HOLCF/Fixrec.thy	Sun Nov 02 17:14:15 2014 +0100
    20.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Sun Nov 02 17:16:01 2014 +0100
    20.3 @@ -2,7 +2,7 @@
    20.4      Author:     Amber Telfer and Brian Huffman
    20.5  *)
    20.6  
    20.7 -header "Package for defining recursive functions in HOLCF"
    20.8 +section "Package for defining recursive functions in HOLCF"
    20.9  
   20.10  theory Fixrec
   20.11  imports Plain_HOLCF
    21.1 --- a/src/HOL/HOLCF/Fun_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
    21.2 +++ b/src/HOL/HOLCF/Fun_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
    21.3 @@ -3,7 +3,7 @@
    21.4      Author:     Brian Huffman
    21.5  *)
    21.6  
    21.7 -header {* Class instances for the full function space *}
    21.8 +section {* Class instances for the full function space *}
    21.9  
   21.10  theory Fun_Cpo
   21.11  imports Adm
    22.1 --- a/src/HOL/HOLCF/IMP/Denotational.thy	Sun Nov 02 17:14:15 2014 +0100
    22.2 +++ b/src/HOL/HOLCF/IMP/Denotational.thy	Sun Nov 02 17:16:01 2014 +0100
    22.3 @@ -3,7 +3,7 @@
    22.4      Copyright   1996 TUM
    22.5  *)
    22.6  
    22.7 -header "Denotational Semantics of Commands in HOLCF"
    22.8 +section "Denotational Semantics of Commands in HOLCF"
    22.9  
   22.10  theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
   22.11  
    23.1 --- a/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Nov 02 17:14:15 2014 +0100
    23.2 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Nov 02 17:16:01 2014 +0100
    23.3 @@ -3,7 +3,7 @@
    23.4      Copyright   1997 TUM
    23.5  *)
    23.6  
    23.7 -header "Correctness of Hoare by Fixpoint Reasoning"
    23.8 +section "Correctness of Hoare by Fixpoint Reasoning"
    23.9  
   23.10  theory HoareEx imports Denotational begin
   23.11  
    24.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Sun Nov 02 17:14:15 2014 +0100
    24.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Sun Nov 02 17:16:01 2014 +0100
    24.3 @@ -2,7 +2,7 @@
    24.4      Author:     Olaf Müller
    24.5  *)
    24.6  
    24.7 -header {* The transmission channel *}
    24.8 +section {* The transmission channel *}
    24.9  
   24.10  theory Abschannel
   24.11  imports IOA Action Lemmas
    25.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Sun Nov 02 17:14:15 2014 +0100
    25.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Sun Nov 02 17:16:01 2014 +0100
    25.3 @@ -2,7 +2,7 @@
    25.4      Author:     Olaf Müller
    25.5  *)
    25.6  
    25.7 -header {* The transmission channel -- finite version *}
    25.8 +section {* The transmission channel -- finite version *}
    25.9  
   25.10  theory Abschannel_finite
   25.11  imports Abschannel IOA Action Lemmas
    26.1 --- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Sun Nov 02 17:14:15 2014 +0100
    26.2 +++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Sun Nov 02 17:16:01 2014 +0100
    26.3 @@ -2,7 +2,7 @@
    26.4      Author:     Olaf Müller
    26.5  *)
    26.6  
    26.7 -header {* The set of all actions of the system *}
    26.8 +section {* The set of all actions of the system *}
    26.9  
   26.10  theory Action
   26.11  imports Packet
    27.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Nov 02 17:14:15 2014 +0100
    27.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Nov 02 17:16:01 2014 +0100
    27.3 @@ -2,7 +2,7 @@
    27.4      Author:     Olaf Müller
    27.5  *)
    27.6  
    27.7 -header {* The main correctness proof: System_fin implements System *}
    27.8 +section {* The main correctness proof: System_fin implements System *}
    27.9  
   27.10  theory Correctness
   27.11  imports IOA Env Impl Impl_finite
    28.1 --- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Sun Nov 02 17:14:15 2014 +0100
    28.2 +++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Sun Nov 02 17:16:01 2014 +0100
    28.3 @@ -2,7 +2,7 @@
    28.4      Author:     Olaf Müller
    28.5  *)
    28.6  
    28.7 -header {* The environment *}
    28.8 +section {* The environment *}
    28.9  
   28.10  theory Env
   28.11  imports IOA Action
    29.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sun Nov 02 17:14:15 2014 +0100
    29.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sun Nov 02 17:16:01 2014 +0100
    29.3 @@ -2,7 +2,7 @@
    29.4      Author:     Olaf Müller
    29.5  *)
    29.6  
    29.7 -header {* The implementation *}
    29.8 +section {* The implementation *}
    29.9  
   29.10  theory Impl
   29.11  imports Sender Receiver Abschannel
    30.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sun Nov 02 17:14:15 2014 +0100
    30.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sun Nov 02 17:16:01 2014 +0100
    30.3 @@ -2,7 +2,7 @@
    30.4      Author:     Olaf Müller
    30.5  *)
    30.6  
    30.7 -header {* The implementation *}
    30.8 +section {* The implementation *}
    30.9  
   30.10  theory Impl_finite
   30.11  imports Sender Receiver Abschannel_finite
    31.1 --- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sun Nov 02 17:14:15 2014 +0100
    31.2 +++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sun Nov 02 17:16:01 2014 +0100
    31.3 @@ -2,7 +2,7 @@
    31.4      Author:     Olaf Müller
    31.5  *)
    31.6  
    31.7 -header {* Packets *}
    31.8 +section {* Packets *}
    31.9  
   31.10  theory Packet
   31.11  imports Main
    32.1 --- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sun Nov 02 17:14:15 2014 +0100
    32.2 +++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sun Nov 02 17:16:01 2014 +0100
    32.3 @@ -2,7 +2,7 @@
    32.4      Author:     Olaf Müller
    32.5  *)
    32.6  
    32.7 -header {* The implementation: receiver *}
    32.8 +section {* The implementation: receiver *}
    32.9  
   32.10  theory Receiver
   32.11  imports IOA Action Lemmas
    33.1 --- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sun Nov 02 17:14:15 2014 +0100
    33.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sun Nov 02 17:16:01 2014 +0100
    33.3 @@ -2,7 +2,7 @@
    33.4      Author:     Olaf Müller
    33.5  *)
    33.6  
    33.7 -header {* The implementation: sender *}
    33.8 +section {* The implementation: sender *}
    33.9  
   33.10  theory Sender
   33.11  imports IOA Action Lemmas
    34.1 --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Nov 02 17:14:15 2014 +0100
    34.2 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Nov 02 17:16:01 2014 +0100
    34.3 @@ -2,7 +2,7 @@
    34.4      Author:     Olaf Müller
    34.5  *)
    34.6  
    34.7 -header {* The specification of reliable transmission *}
    34.8 +section {* The specification of reliable transmission *}
    34.9  
   34.10  theory Spec
   34.11  imports IOA Action
    35.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Sun Nov 02 17:14:15 2014 +0100
    35.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Sun Nov 02 17:16:01 2014 +0100
    35.3 @@ -2,7 +2,7 @@
    35.4      Author:     Olaf Müller
    35.5  *)
    35.6  
    35.7 -header {* The (faulty) transmission channel (both directions) *}
    35.8 +section {* The (faulty) transmission channel (both directions) *}
    35.9  
   35.10  theory Abschannel
   35.11  imports IOA Action
    36.1 --- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Sun Nov 02 17:14:15 2014 +0100
    36.2 +++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Sun Nov 02 17:16:01 2014 +0100
    36.3 @@ -2,7 +2,7 @@
    36.4      Author:     Tobias Nipkow & Konrad Slind
    36.5  *)
    36.6  
    36.7 -header {* The set of all actions of the system *}
    36.8 +section {* The set of all actions of the system *}
    36.9  
   36.10  theory Action
   36.11  imports Packet
    37.1 --- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Sun Nov 02 17:14:15 2014 +0100
    37.2 +++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Sun Nov 02 17:16:01 2014 +0100
    37.3 @@ -2,7 +2,7 @@
    37.4      Author:     Tobias Nipkow & Konrad Slind
    37.5  *)
    37.6  
    37.7 -header {* The main correctness proof: Impl implements Spec *}
    37.8 +section {* The main correctness proof: Impl implements Spec *}
    37.9  
   37.10  theory Correctness
   37.11  imports Impl Spec
    38.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sun Nov 02 17:14:15 2014 +0100
    38.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sun Nov 02 17:16:01 2014 +0100
    38.3 @@ -2,7 +2,7 @@
    38.4      Author:     Tobias Nipkow & Konrad Slind
    38.5  *)
    38.6  
    38.7 -header {* The implementation *}
    38.8 +section {* The implementation *}
    38.9  
   38.10  theory Impl
   38.11  imports Sender Receiver Abschannel
    39.1 --- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Sun Nov 02 17:14:15 2014 +0100
    39.2 +++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Sun Nov 02 17:16:01 2014 +0100
    39.3 @@ -2,7 +2,7 @@
    39.4      Author:     Tobias Nipkow & Konrad Slind
    39.5  *)
    39.6  
    39.7 -header {* Axiomatic multisets *}
    39.8 +section {* Axiomatic multisets *}
    39.9  
   39.10  theory Multiset
   39.11  imports Lemmas
    40.1 --- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sun Nov 02 17:14:15 2014 +0100
    40.2 +++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sun Nov 02 17:16:01 2014 +0100
    40.3 @@ -2,7 +2,7 @@
    40.4      Author:     Tobias Nipkow & Konrad Slind
    40.5  *)
    40.6  
    40.7 -header {* The implementation: receiver *}
    40.8 +section {* The implementation: receiver *}
    40.9  
   40.10  theory Receiver
   40.11  imports IOA Action
    41.1 --- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sun Nov 02 17:14:15 2014 +0100
    41.2 +++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sun Nov 02 17:16:01 2014 +0100
    41.3 @@ -2,7 +2,7 @@
    41.4      Author:     Tobias Nipkow & Konrad Slind
    41.5  *)
    41.6  
    41.7 -header {* The implementation: sender *}
    41.8 +section {* The implementation: sender *}
    41.9  
   41.10  theory Sender
   41.11  imports IOA Action
    42.1 --- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Sun Nov 02 17:14:15 2014 +0100
    42.2 +++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Sun Nov 02 17:16:01 2014 +0100
    42.3 @@ -2,7 +2,7 @@
    42.4      Author:     Tobias Nipkow & Konrad Slind
    42.5  *)
    42.6  
    42.7 -header {* The specification of reliable transmission *}
    42.8 +section {* The specification of reliable transmission *}
    42.9  
   42.10  theory Spec
   42.11  imports IOA Action
    43.1 --- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Sun Nov 02 17:14:15 2014 +0100
    43.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Sun Nov 02 17:16:01 2014 +0100
    43.3 @@ -2,7 +2,7 @@
    43.4      Author:     Olaf Müller
    43.5  *)
    43.6  
    43.7 -header {* The set of all actions of the system *}
    43.8 +section {* The set of all actions of the system *}
    43.9  
   43.10  theory Action
   43.11  imports Main
    44.1 --- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Sun Nov 02 17:14:15 2014 +0100
    44.2 +++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Sun Nov 02 17:16:01 2014 +0100
    44.3 @@ -2,7 +2,7 @@
    44.4      Author:     Olaf Müller
    44.5  *)
    44.6  
    44.7 -header {* Correctness Proof *}
    44.8 +section {* Correctness Proof *}
    44.9  
   44.10  theory Correctness
   44.11  imports SimCorrectness Spec Impl
    45.1 --- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Sun Nov 02 17:14:15 2014 +0100
    45.2 +++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Sun Nov 02 17:16:01 2014 +0100
    45.3 @@ -2,7 +2,7 @@
    45.4      Author:     Olaf Müller
    45.5  *)
    45.6  
    45.7 -header {* The implementation of a memory *}
    45.8 +section {* The implementation of a memory *}
    45.9  
   45.10  theory Impl
   45.11  imports IOA Action
    46.1 --- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Sun Nov 02 17:14:15 2014 +0100
    46.2 +++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Sun Nov 02 17:16:01 2014 +0100
    46.3 @@ -2,7 +2,7 @@
    46.4      Author:     Olaf Müller
    46.5  *)
    46.6  
    46.7 -header {* The specification of a memory *}
    46.8 +section {* The specification of a memory *}
    46.9  
   46.10  theory Spec
   46.11  imports IOA Action
    47.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Sun Nov 02 17:14:15 2014 +0100
    47.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Sun Nov 02 17:16:01 2014 +0100
    47.3 @@ -2,7 +2,7 @@
    47.4      Author:     Olaf Müller
    47.5  *)
    47.6  
    47.7 -header {* Trivial Abstraction Example *}
    47.8 +section {* Trivial Abstraction Example *}
    47.9  
   47.10  theory TrivEx
   47.11  imports Abstraction
    48.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Sun Nov 02 17:14:15 2014 +0100
    48.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Sun Nov 02 17:16:01 2014 +0100
    48.3 @@ -2,7 +2,7 @@
    48.4      Author:     Olaf Müller
    48.5  *)
    48.6  
    48.7 -header {* Trivial Abstraction Example with fairness *}
    48.8 +section {* Trivial Abstraction Example with fairness *}
    48.9  
   48.10  theory TrivEx2
   48.11  imports IOA Abstraction
    49.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Nov 02 17:14:15 2014 +0100
    49.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Nov 02 17:16:01 2014 +0100
    49.3 @@ -2,7 +2,7 @@
    49.4      Author:     Olaf Müller
    49.5  *)
    49.6  
    49.7 -header {* Abstraction Theory -- tailored for I/O automata *}
    49.8 +section {* Abstraction Theory -- tailored for I/O automata *}
    49.9  
   49.10  theory Abstraction
   49.11  imports LiveIOA
    50.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sun Nov 02 17:14:15 2014 +0100
    50.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sun Nov 02 17:16:01 2014 +0100
    50.3 @@ -2,7 +2,7 @@
    50.4      Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    50.5  *)
    50.6  
    50.7 -header {* Action signatures *}
    50.8 +section {* Action signatures *}
    50.9  
   50.10  theory Asig
   50.11  imports Main
    51.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 02 17:14:15 2014 +0100
    51.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 02 17:16:01 2014 +0100
    51.3 @@ -2,7 +2,7 @@
    51.4      Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
    51.5  *)
    51.6  
    51.7 -header {* The I/O automata of Lynch and Tuttle in HOLCF *}
    51.8 +section {* The I/O automata of Lynch and Tuttle in HOLCF *}
    51.9  
   51.10  theory Automata
   51.11  imports Asig
    52.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Sun Nov 02 17:14:15 2014 +0100
    52.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Sun Nov 02 17:16:01 2014 +0100
    52.3 @@ -2,7 +2,7 @@
    52.4      Author:     Olaf Müller
    52.5  *)
    52.6  
    52.7 -header {* Compositionality on Execution level *}
    52.8 +section {* Compositionality on Execution level *}
    52.9  
   52.10  theory CompoExecs
   52.11  imports Traces
    53.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 02 17:14:15 2014 +0100
    53.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 02 17:16:01 2014 +0100
    53.3 @@ -2,7 +2,7 @@
    53.4      Author:     Olaf Müller
    53.5  *)
    53.6  
    53.7 -header {* Compositionality on Schedule level *}
    53.8 +section {* Compositionality on Schedule level *}
    53.9  
   53.10  theory CompoScheds
   53.11  imports CompoExecs
    54.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Nov 02 17:14:15 2014 +0100
    54.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Nov 02 17:16:01 2014 +0100
    54.3 @@ -2,7 +2,7 @@
    54.4      Author:     Olaf Müller
    54.5  *) 
    54.6  
    54.7 -header {* Compositionality on Trace level *}
    54.8 +section {* Compositionality on Trace level *}
    54.9  
   54.10  theory CompoTraces
   54.11  imports CompoScheds ShortExecutions
    55.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Sun Nov 02 17:14:15 2014 +0100
    55.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Sun Nov 02 17:16:01 2014 +0100
    55.3 @@ -2,7 +2,7 @@
    55.4      Author:     Olaf Müller
    55.5  *)
    55.6  
    55.7 -header {* Compositionality of I/O automata *}
    55.8 +section {* Compositionality of I/O automata *}
    55.9  theory Compositionality
   55.10  imports CompoTraces
   55.11  begin
    56.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Sun Nov 02 17:14:15 2014 +0100
    56.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Sun Nov 02 17:16:01 2014 +0100
    56.3 @@ -2,7 +2,7 @@
    56.4      Author:     Olaf Müller
    56.5  *)
    56.6  
    56.7 -header {* Deadlock freedom of I/O Automata *}
    56.8 +section {* Deadlock freedom of I/O Automata *}
    56.9  
   56.10  theory Deadlock
   56.11  imports RefCorrectness CompoScheds
    57.1 --- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Sun Nov 02 17:14:15 2014 +0100
    57.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Sun Nov 02 17:16:01 2014 +0100
    57.3 @@ -2,7 +2,7 @@
    57.4      Author:     Olaf Müller
    57.5  *)
    57.6  
    57.7 -header {* The theory of I/O automata in HOLCF *}
    57.8 +section {* The theory of I/O automata in HOLCF *}
    57.9  
   57.10  theory IOA
   57.11  imports SimCorrectness Compositionality Deadlock
    58.1 --- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun Nov 02 17:14:15 2014 +0100
    58.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sun Nov 02 17:16:01 2014 +0100
    58.3 @@ -2,7 +2,7 @@
    58.4      Author:     Olaf Müller
    58.5  *)
    58.6  
    58.7 -header {* Live I/O automata -- specified by temproal formulas *}
    58.8 +section {* Live I/O automata -- specified by temproal formulas *}
    58.9  
   58.10  theory LiveIOA
   58.11  imports TLS
    59.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sun Nov 02 17:14:15 2014 +0100
    59.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sun Nov 02 17:16:01 2014 +0100
    59.3 @@ -2,7 +2,7 @@
    59.4      Author:     Olaf Müller
    59.5  *)
    59.6  
    59.7 -header {* Logical Connectives lifted to predicates *}
    59.8 +section {* Logical Connectives lifted to predicates *}
    59.9  
   59.10  theory Pred
   59.11  imports Main
    60.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sun Nov 02 17:14:15 2014 +0100
    60.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sun Nov 02 17:16:01 2014 +0100
    60.3 @@ -2,7 +2,7 @@
    60.4      Author:     Olaf Müller
    60.5  *)
    60.6  
    60.7 -header {* Correctness of Refinement Mappings in HOLCF/IOA *}
    60.8 +section {* Correctness of Refinement Mappings in HOLCF/IOA *}
    60.9  
   60.10  theory RefCorrectness
   60.11  imports RefMappings
    61.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Sun Nov 02 17:14:15 2014 +0100
    61.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Sun Nov 02 17:16:01 2014 +0100
    61.3 @@ -2,7 +2,7 @@
    61.4      Author:     Olaf Müller
    61.5  *)
    61.6  
    61.7 -header {* Refinement Mappings in HOLCF/IOA *}
    61.8 +section {* Refinement Mappings in HOLCF/IOA *}
    61.9  
   61.10  theory RefMappings
   61.11  imports Traces
    62.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Sun Nov 02 17:14:15 2014 +0100
    62.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Sun Nov 02 17:16:01 2014 +0100
    62.3 @@ -2,7 +2,7 @@
    62.4      Author:     Olaf Müller
    62.5  *)
    62.6  
    62.7 -header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
    62.8 +section {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
    62.9  
   62.10  theory Seq
   62.11  imports "../../HOLCF"
    63.1 --- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sun Nov 02 17:14:15 2014 +0100
    63.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sun Nov 02 17:16:01 2014 +0100
    63.3 @@ -2,7 +2,7 @@
    63.4      Author:     Olaf Müller
    63.5  *)
    63.6  
    63.7 -header {* Correctness of Simulations in HOLCF/IOA *}
    63.8 +section {* Correctness of Simulations in HOLCF/IOA *}
    63.9  
   63.10  theory SimCorrectness
   63.11  imports Simulations
    64.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Sun Nov 02 17:14:15 2014 +0100
    64.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Sun Nov 02 17:16:01 2014 +0100
    64.3 @@ -2,7 +2,7 @@
    64.4      Author:     Olaf Müller
    64.5  *)
    64.6  
    64.7 -header {* Simulations in HOLCF/IOA *}
    64.8 +section {* Simulations in HOLCF/IOA *}
    64.9  
   64.10  theory Simulations
   64.11  imports RefCorrectness
    65.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sun Nov 02 17:14:15 2014 +0100
    65.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sun Nov 02 17:16:01 2014 +0100
    65.3 @@ -2,7 +2,7 @@
    65.4      Author:     Olaf Müller
    65.5  *)
    65.6  
    65.7 -header {* A General Temporal Logic *}
    65.8 +section {* A General Temporal Logic *}
    65.9  
   65.10  theory TL
   65.11  imports Pred Sequence
    66.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sun Nov 02 17:14:15 2014 +0100
    66.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sun Nov 02 17:16:01 2014 +0100
    66.3 @@ -2,7 +2,7 @@
    66.4      Author:     Olaf Müller
    66.5  *)
    66.6  
    66.7 -header {* Temporal Logic of Steps -- tailored for I/O automata *}
    66.8 +section {* Temporal Logic of Steps -- tailored for I/O automata *}
    66.9  
   66.10  theory TLS
   66.11  imports IOA TL
    67.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sun Nov 02 17:14:15 2014 +0100
    67.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sun Nov 02 17:16:01 2014 +0100
    67.3 @@ -2,7 +2,7 @@
    67.4      Author:     Olaf Müller
    67.5  *)
    67.6  
    67.7 -header {* Executions and Traces of I/O automata in HOLCF *}
    67.8 +section {* Executions and Traces of I/O automata in HOLCF *}
    67.9  
   67.10  theory Traces
   67.11  imports Sequence Automata
    68.1 --- a/src/HOL/HOLCF/Library/Bool_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
    68.2 +++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
    68.3 @@ -2,7 +2,7 @@
    68.4      Author:     Brian Huffman
    68.5  *)
    68.6  
    68.7 -header {* Discrete cpo instance for booleans *}
    68.8 +section {* Discrete cpo instance for booleans *}
    68.9  
   68.10  theory Bool_Discrete
   68.11  imports HOLCF
    69.1 --- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
    69.2 +++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
    69.3 @@ -2,7 +2,7 @@
    69.4      Author:     Brian Huffman
    69.5  *)
    69.6  
    69.7 -header {* Discrete cpo instance for 8-bit char type *}
    69.8 +section {* Discrete cpo instance for 8-bit char type *}
    69.9  
   69.10  theory Char_Discrete
   69.11  imports HOLCF
    70.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Nov 02 17:14:15 2014 +0100
    70.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Nov 02 17:16:01 2014 +0100
    70.3 @@ -2,7 +2,7 @@
    70.4      Author:     Brian Huffman
    70.5  *)
    70.6  
    70.7 -header {* Algebraic deflations are a bifinite domain *}
    70.8 +section {* Algebraic deflations are a bifinite domain *}
    70.9  
   70.10  theory Defl_Bifinite
   70.11  imports HOLCF "~~/src/HOL/Library/Infinite_Set"
    71.1 --- a/src/HOL/HOLCF/Library/HOL_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
    71.2 +++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
    71.3 @@ -2,7 +2,7 @@
    71.4      Author:     Brian Huffman
    71.5  *)
    71.6  
    71.7 -header {* Cpo class instances for all HOL types *}
    71.8 +section {* Cpo class instances for all HOL types *}
    71.9  
   71.10  theory HOL_Cpo
   71.11  imports
    72.1 --- a/src/HOL/HOLCF/Library/Int_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
    72.2 +++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
    72.3 @@ -2,7 +2,7 @@
    72.4      Author:     Brian Huffman
    72.5  *)
    72.6  
    72.7 -header {* Discrete cpo instance for integers *}
    72.8 +section {* Discrete cpo instance for integers *}
    72.9  
   72.10  theory Int_Discrete
   72.11  imports HOLCF
    73.1 --- a/src/HOL/HOLCF/Library/List_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
    73.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
    73.3 @@ -2,7 +2,7 @@
    73.4      Author:     Brian Huffman
    73.5  *)
    73.6  
    73.7 -header {* Lists as a complete partial order *}
    73.8 +section {* Lists as a complete partial order *}
    73.9  
   73.10  theory List_Cpo
   73.11  imports HOLCF
    74.1 --- a/src/HOL/HOLCF/Library/List_Predomain.thy	Sun Nov 02 17:14:15 2014 +0100
    74.2 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Sun Nov 02 17:16:01 2014 +0100
    74.3 @@ -2,7 +2,7 @@
    74.4      Author:     Brian Huffman
    74.5  *)
    74.6  
    74.7 -header {* Predomain class instance for HOL list type *}
    74.8 +section {* Predomain class instance for HOL list type *}
    74.9  
   74.10  theory List_Predomain
   74.11  imports List_Cpo Sum_Cpo
    75.1 --- a/src/HOL/HOLCF/Library/Nat_Discrete.thy	Sun Nov 02 17:14:15 2014 +0100
    75.2 +++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
    75.3 @@ -2,7 +2,7 @@
    75.4      Author:     Brian Huffman
    75.5  *)
    75.6  
    75.7 -header {* Discrete cpo instance for naturals *}
    75.8 +section {* Discrete cpo instance for naturals *}
    75.9  
   75.10  theory Nat_Discrete
   75.11  imports HOLCF
    76.1 --- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
    76.2 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
    76.3 @@ -2,7 +2,7 @@
    76.4      Author:     Brian Huffman
    76.5  *)
    76.6  
    76.7 -header {* Cpo class instance for HOL option type *}
    76.8 +section {* Cpo class instance for HOL option type *}
    76.9  
   76.10  theory Option_Cpo
   76.11  imports HOLCF Sum_Cpo
    77.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Sun Nov 02 17:14:15 2014 +0100
    77.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Sun Nov 02 17:16:01 2014 +0100
    77.3 @@ -2,7 +2,7 @@
    77.4      Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
    77.5  *)
    77.6  
    77.7 -header {* General Stream domain *}
    77.8 +section {* General Stream domain *}
    77.9  
   77.10  theory Stream
   77.11  imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
    78.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
    78.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
    78.3 @@ -2,7 +2,7 @@
    78.4      Author:     Brian Huffman
    78.5  *)
    78.6  
    78.7 -header {* The cpo of disjoint sums *}
    78.8 +section {* The cpo of disjoint sums *}
    78.9  
   78.10  theory Sum_Cpo
   78.11  imports HOLCF
    79.1 --- a/src/HOL/HOLCF/Lift.thy	Sun Nov 02 17:14:15 2014 +0100
    79.2 +++ b/src/HOL/HOLCF/Lift.thy	Sun Nov 02 17:16:01 2014 +0100
    79.3 @@ -2,7 +2,7 @@
    79.4      Author:     Olaf Mueller
    79.5  *)
    79.6  
    79.7 -header {* Lifting types of class type to flat pcpo's *}
    79.8 +section {* Lifting types of class type to flat pcpo's *}
    79.9  
   79.10  theory Lift
   79.11  imports Discrete Up
    80.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Nov 02 17:14:15 2014 +0100
    80.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Nov 02 17:16:01 2014 +0100
    80.3 @@ -2,7 +2,7 @@
    80.4      Author:     Brian Huffman
    80.5  *)
    80.6  
    80.7 -header {* Lower powerdomain *}
    80.8 +section {* Lower powerdomain *}
    80.9  
   80.10  theory LowerPD
   80.11  imports Compact_Basis
    81.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Sun Nov 02 17:14:15 2014 +0100
    81.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Nov 02 17:16:01 2014 +0100
    81.3 @@ -2,7 +2,7 @@
    81.4      Author:     Brian Huffman
    81.5  *)
    81.6  
    81.7 -header {* Map functions for various types *}
    81.8 +section {* Map functions for various types *}
    81.9  
   81.10  theory Map_Functions
   81.11  imports Deflation
    82.1 --- a/src/HOL/HOLCF/One.thy	Sun Nov 02 17:14:15 2014 +0100
    82.2 +++ b/src/HOL/HOLCF/One.thy	Sun Nov 02 17:16:01 2014 +0100
    82.3 @@ -2,7 +2,7 @@
    82.4      Author:     Oscar Slotosch
    82.5  *)
    82.6  
    82.7 -header {* The unit domain *}
    82.8 +section {* The unit domain *}
    82.9  
   82.10  theory One
   82.11  imports Lift
    83.1 --- a/src/HOL/HOLCF/Pcpo.thy	Sun Nov 02 17:14:15 2014 +0100
    83.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Sun Nov 02 17:16:01 2014 +0100
    83.3 @@ -2,7 +2,7 @@
    83.4      Author:     Franz Regensburger
    83.5  *)
    83.6  
    83.7 -header {* Classes cpo and pcpo *}
    83.8 +section {* Classes cpo and pcpo *}
    83.9  
   83.10  theory Pcpo
   83.11  imports Porder
    84.1 --- a/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Nov 02 17:14:15 2014 +0100
    84.2 +++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Nov 02 17:16:01 2014 +0100
    84.3 @@ -2,7 +2,7 @@
    84.4      Author:     Brian Huffman
    84.5  *)
    84.6  
    84.7 -header {* Plain HOLCF *}
    84.8 +section {* Plain HOLCF *}
    84.9  
   84.10  theory Plain_HOLCF
   84.11  imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
    85.1 --- a/src/HOL/HOLCF/Porder.thy	Sun Nov 02 17:14:15 2014 +0100
    85.2 +++ b/src/HOL/HOLCF/Porder.thy	Sun Nov 02 17:16:01 2014 +0100
    85.3 @@ -2,7 +2,7 @@
    85.4      Author:     Franz Regensburger and Brian Huffman
    85.5  *)
    85.6  
    85.7 -header {* Partial orders *}
    85.8 +section {* Partial orders *}
    85.9  
   85.10  theory Porder
   85.11  imports Main
    86.1 --- a/src/HOL/HOLCF/Powerdomains.thy	Sun Nov 02 17:14:15 2014 +0100
    86.2 +++ b/src/HOL/HOLCF/Powerdomains.thy	Sun Nov 02 17:16:01 2014 +0100
    86.3 @@ -2,7 +2,7 @@
    86.4      Author:     Brian Huffman
    86.5  *)
    86.6  
    86.7 -header {* Powerdomains *}
    86.8 +section {* Powerdomains *}
    86.9  
   86.10  theory Powerdomains
   86.11  imports ConvexPD Domain
    87.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Sun Nov 02 17:14:15 2014 +0100
    87.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Sun Nov 02 17:16:01 2014 +0100
    87.3 @@ -2,7 +2,7 @@
    87.4      Author:     Franz Regensburger
    87.5  *)
    87.6  
    87.7 -header {* The cpo of cartesian products *}
    87.8 +section {* The cpo of cartesian products *}
    87.9  
   87.10  theory Product_Cpo
   87.11  imports Adm
    88.1 --- a/src/HOL/HOLCF/Representable.thy	Sun Nov 02 17:14:15 2014 +0100
    88.2 +++ b/src/HOL/HOLCF/Representable.thy	Sun Nov 02 17:16:01 2014 +0100
    88.3 @@ -2,7 +2,7 @@
    88.4      Author:     Brian Huffman
    88.5  *)
    88.6  
    88.7 -header {* Representable domains *}
    88.8 +section {* Representable domains *}
    88.9  
   88.10  theory Representable
   88.11  imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
    89.1 --- a/src/HOL/HOLCF/Sfun.thy	Sun Nov 02 17:14:15 2014 +0100
    89.2 +++ b/src/HOL/HOLCF/Sfun.thy	Sun Nov 02 17:16:01 2014 +0100
    89.3 @@ -2,7 +2,7 @@
    89.4      Author:     Brian Huffman
    89.5  *)
    89.6  
    89.7 -header {* The Strict Function Type *}
    89.8 +section {* The Strict Function Type *}
    89.9  
   89.10  theory Sfun
   89.11  imports Cfun
    90.1 --- a/src/HOL/HOLCF/Sprod.thy	Sun Nov 02 17:14:15 2014 +0100
    90.2 +++ b/src/HOL/HOLCF/Sprod.thy	Sun Nov 02 17:16:01 2014 +0100
    90.3 @@ -3,7 +3,7 @@
    90.4      Author:     Brian Huffman
    90.5  *)
    90.6  
    90.7 -header {* The type of strict products *}
    90.8 +section {* The type of strict products *}
    90.9  
   90.10  theory Sprod
   90.11  imports Cfun
    91.1 --- a/src/HOL/HOLCF/Ssum.thy	Sun Nov 02 17:14:15 2014 +0100
    91.2 +++ b/src/HOL/HOLCF/Ssum.thy	Sun Nov 02 17:16:01 2014 +0100
    91.3 @@ -3,7 +3,7 @@
    91.4      Author:     Brian Huffman
    91.5  *)
    91.6  
    91.7 -header {* The type of strict sums *}
    91.8 +section {* The type of strict sums *}
    91.9  
   91.10  theory Ssum
   91.11  imports Tr
    92.1 --- a/src/HOL/HOLCF/Tr.thy	Sun Nov 02 17:14:15 2014 +0100
    92.2 +++ b/src/HOL/HOLCF/Tr.thy	Sun Nov 02 17:16:01 2014 +0100
    92.3 @@ -2,7 +2,7 @@
    92.4      Author:     Franz Regensburger
    92.5  *)
    92.6  
    92.7 -header {* The type of lifted booleans *}
    92.8 +section {* The type of lifted booleans *}
    92.9  
   92.10  theory Tr
   92.11  imports Lift
    93.1 --- a/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Sun Nov 02 17:14:15 2014 +0100
    93.2 +++ b/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Sun Nov 02 17:16:01 2014 +0100
    93.3 @@ -2,7 +2,7 @@
    93.4      Author:     Brian Huffman
    93.5  *)
    93.6  
    93.7 -header {* Domain package examples *}
    93.8 +section {* Domain package examples *}
    93.9  
   93.10  theory Domain_ex
   93.11  imports HOLCF
    94.1 --- a/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Sun Nov 02 17:14:15 2014 +0100
    94.2 +++ b/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Sun Nov 02 17:16:01 2014 +0100
    94.3 @@ -2,7 +2,7 @@
    94.4      Author:     Brian Huffman
    94.5  *)
    94.6  
    94.7 -header {* Fixrec package examples *}
    94.8 +section {* Fixrec package examples *}
    94.9  
   94.10  theory Fixrec_ex
   94.11  imports HOLCF
    95.1 --- a/src/HOL/HOLCF/Tutorial/New_Domain.thy	Sun Nov 02 17:14:15 2014 +0100
    95.2 +++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Sun Nov 02 17:16:01 2014 +0100
    95.3 @@ -2,7 +2,7 @@
    95.4      Author:     Brian Huffman
    95.5  *)
    95.6  
    95.7 -header {* Definitional domain package *}
    95.8 +section {* Definitional domain package *}
    95.9  
   95.10  theory New_Domain
   95.11  imports HOLCF
    96.1 --- a/src/HOL/HOLCF/Universal.thy	Sun Nov 02 17:14:15 2014 +0100
    96.2 +++ b/src/HOL/HOLCF/Universal.thy	Sun Nov 02 17:16:01 2014 +0100
    96.3 @@ -2,7 +2,7 @@
    96.4      Author:     Brian Huffman
    96.5  *)
    96.6  
    96.7 -header {* A universal bifinite domain *}
    96.8 +section {* A universal bifinite domain *}
    96.9  
   96.10  theory Universal
   96.11  imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
    97.1 --- a/src/HOL/HOLCF/Up.thy	Sun Nov 02 17:14:15 2014 +0100
    97.2 +++ b/src/HOL/HOLCF/Up.thy	Sun Nov 02 17:16:01 2014 +0100
    97.3 @@ -3,7 +3,7 @@
    97.4      Author:     Brian Huffman
    97.5  *)
    97.6  
    97.7 -header {* The type of lifted values *}
    97.8 +section {* The type of lifted values *}
    97.9  
   97.10  theory Up
   97.11  imports Cfun
    98.1 --- a/src/HOL/HOLCF/UpperPD.thy	Sun Nov 02 17:14:15 2014 +0100
    98.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Sun Nov 02 17:16:01 2014 +0100
    98.3 @@ -2,7 +2,7 @@
    98.4      Author:     Brian Huffman
    98.5  *)
    98.6  
    98.7 -header {* Upper powerdomain *}
    98.8 +section {* Upper powerdomain *}
    98.9  
   98.10  theory UpperPD
   98.11  imports Compact_Basis
    99.1 --- a/src/HOL/HOLCF/document/root.tex	Sun Nov 02 17:14:15 2014 +0100
    99.2 +++ b/src/HOL/HOLCF/document/root.tex	Sun Nov 02 17:16:01 2014 +0100
    99.3 @@ -27,8 +27,7 @@
    99.4  
    99.5  \newpage
    99.6  
    99.7 -\renewcommand{\isamarkupheader}[1]%
    99.8 -{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
    99.9 +\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
   99.10  
   99.11  \parindent 0pt\parskip 0.5ex
   99.12  \input{session}
   100.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Nov 02 17:14:15 2014 +0100
   100.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Nov 02 17:16:01 2014 +0100
   100.3 @@ -2,7 +2,7 @@
   100.4      Author:     Brian Huffman
   100.5  *)
   100.6  
   100.7 -header {* Internal domain package proofs done manually *}
   100.8 +section {* Internal domain package proofs done manually *}
   100.9  
  100.10  theory Domain_Proofs
  100.11  imports HOLCF
   101.1 --- a/src/HOL/HOLCF/ex/Letrec.thy	Sun Nov 02 17:14:15 2014 +0100
   101.2 +++ b/src/HOL/HOLCF/ex/Letrec.thy	Sun Nov 02 17:16:01 2014 +0100
   101.3 @@ -2,7 +2,7 @@
   101.4      Author:     Brian Huffman
   101.5  *)
   101.6  
   101.7 -header {* Recursive let bindings *}
   101.8 +section {* Recursive let bindings *}
   101.9  
  101.10  theory Letrec
  101.11  imports HOLCF
   102.1 --- a/src/HOL/HOLCF/ex/Loop.thy	Sun Nov 02 17:14:15 2014 +0100
   102.2 +++ b/src/HOL/HOLCF/ex/Loop.thy	Sun Nov 02 17:16:01 2014 +0100
   102.3 @@ -2,7 +2,7 @@
   102.4      Author:     Franz Regensburger
   102.5  *)
   102.6  
   102.7 -header {* Theory for a loop primitive like while *}
   102.8 +section {* Theory for a loop primitive like while *}
   102.9  
  102.10  theory Loop
  102.11  imports HOLCF
   103.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 02 17:14:15 2014 +0100
   103.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 02 17:16:01 2014 +0100
   103.3 @@ -2,7 +2,7 @@
   103.4      Author:     Brian Huffman
   103.5  *)
   103.6  
   103.7 -header {* An experimental pattern-matching notation *}
   103.8 +section {* An experimental pattern-matching notation *}
   103.9  
  103.10  theory Pattern_Match
  103.11  imports HOLCF
   104.1 --- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Sun Nov 02 17:14:15 2014 +0100
   104.2 +++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Sun Nov 02 17:16:01 2014 +0100
   104.3 @@ -2,7 +2,7 @@
   104.4      Author:     Brian Huffman
   104.5  *)
   104.6  
   104.7 -header {* Powerdomain examples *}
   104.8 +section {* Powerdomain examples *}
   104.9  
  104.10  theory Powerdomain_ex
  104.11  imports HOLCF