--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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}
--- 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
--- 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
--- 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
--- 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
--- 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