author wenzelm Sun, 02 Nov 2014 18:21:45 +0100 changeset 58889 5b7a9633cfa8 parent 58888 9537bf1c4853 child 58890 0ca19a9fdc60
--- a/src/CCL/CCL.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/CCL.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Classical Computational Logic for Untyped Lambda Calculus
+section {* Classical Computational Logic for Untyped Lambda Calculus
with reduction to weak head-normal form *}

theory CCL
--- a/src/CCL/Fix.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Fix.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Tentative attempt at including fixed point induction; justified by Smith *}
+section {* Tentative attempt at including fixed point induction; justified by Smith *}

theory Fix
imports Type
--- a/src/CCL/Gfp.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Gfp.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Greatest fixed points *}
+section {* Greatest fixed points *}

theory Gfp
imports Lfp
--- a/src/CCL/Hered.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Hered.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Hereditary Termination -- cf. Martin Lo\"f *}
+section {* Hereditary Termination -- cf. Martin Lo\"f *}

theory Hered
imports Type
--- a/src/CCL/Lfp.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Lfp.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The Knaster-Tarski Theorem *}
+section {* The Knaster-Tarski Theorem *}

theory Lfp
imports Set
--- a/src/CCL/Set.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Set.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* Extending FOL by a modified version of HOL set theory *}
+section {* Extending FOL by a modified version of HOL set theory *}

theory Set
imports "~~/src/FOL/FOL"
--- a/src/CCL/Term.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Term.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Definitions of usual program constructs in CCL *}
+section {* Definitions of usual program constructs in CCL *}

theory Term
imports CCL
--- a/src/CCL/Trancl.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Trancl.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Transitive closure of a relation *}
+section {* Transitive closure of a relation *}

theory Trancl
imports CCL
--- a/src/CCL/Type.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Type.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Types in CCL are defined as sets of terms *}
+section {* Types in CCL are defined as sets of terms *}

theory Type
imports Term
--- a/src/CCL/Wfd.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/Wfd.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Well-founded relations in CCL *}
+section {* Well-founded relations in CCL *}

theory Wfd
imports Trancl Type Hered
--- a/src/CCL/ex/Flag.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/ex/Flag.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Dutch national flag program -- except that the point of Dijkstra's example was to use
+section {* Dutch national flag program -- except that the point of Dijkstra's example was to use
arrays and this uses lists. *}

theory Flag
--- a/src/CCL/ex/List.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/ex/List.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Programs defined over lists *}
+section {* Programs defined over lists *}

theory List
imports Nat
--- a/src/CCL/ex/Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/ex/Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Programs defined over the natural numbers *}
+section {* Programs defined over the natural numbers *}

theory Nat
imports Wfd
--- a/src/CCL/ex/Stream.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CCL/ex/Stream.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Programs defined over streams *}
+section {* Programs defined over streams *}

theory Stream
imports List
--- a/src/CTT/Arith.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/Arith.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Elementary arithmetic *}

theory Arith
imports Bool
--- a/src/CTT/Bool.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/Bool.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The two-element type (booleans and conditionals) *}
+section {* The two-element type (booleans and conditionals) *}

theory Bool
imports CTT
--- a/src/CTT/CTT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/CTT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Constructive Type Theory *}
+section {* Constructive Type Theory *}

theory CTT
imports Pure
--- a/src/CTT/Main.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/Main.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* Main includes everything *}
+section {* Main includes everything *}

theory Main
imports CTT Arith Bool
--- a/src/CTT/ex/Elimination.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/ex/Elimination.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
(Bibliopolis, 1984).
*)

+section "Examples with elimination rules"

theory Elimination
imports CTT
--- a/src/CTT/ex/Equality.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/ex/Equality.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section "Equality reasoning by rewriting"

theory Equality
imports CTT
--- a/src/CTT/ex/Synthesis.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/ex/Synthesis.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header "Synthesis examples, using a crude form of narrowing"
+section "Synthesis examples, using a crude form of narrowing"

theory Synthesis
imports Arith
--- a/src/CTT/ex/Typechecking.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/CTT/ex/Typechecking.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header "Easy examples: type checking and type deduction"
+section "Easy examples: type checking and type deduction"

theory Typechecking
imports CTT
--- a/src/Cube/Cube.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Cube/Cube.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Tobias Nipkow
*)

+section \<open>Barendregt's Lambda-Cube\<close>

theory Cube
imports Pure
--- a/src/Cube/Example.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Cube/Example.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section \<open>Lambda Cube Examples\<close>

theory Example
imports Cube
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,5 +1,5 @@

+section \<open>Example: First-Order Logic\<close>

theory %visible First_Order_Logic
imports Base  (* FIXME Pure!? *)
--- a/src/Doc/Logics_ZF/FOL_examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Logics_ZF/FOL_examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section{*Examples of Classical Reasoning*}

theory FOL_examples imports "~~/src/FOL/FOL" begin

--- a/src/Doc/Logics_ZF/IFOL_examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Logics_ZF/IFOL_examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section{*Examples of Intuitionistic Reasoning*}

theory IFOL_examples imports "~~/src/FOL/IFOL" begin

--- a/src/Doc/Logics_ZF/ZF_examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Logics_ZF/ZF_examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header{*Examples of Reasoning in ZF Set Theory*}
+section{*Examples of Reasoning in ZF Set Theory*}

theory ZF_examples imports Main_ZFC begin

--- a/src/Doc/Tutorial/Protocol/Event.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
stores are visible to him
*)(*<*)

-header{*Theory of Events for Security Protocols*}
+section{*Theory of Events for Security Protocols*}

theory Event imports Message begin

--- a/src/Doc/Tutorial/Protocol/Message.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Inductive relations "parts", "analz" and "synth"
*)(*<*)

-header{*Theory of Agents and Messages for Security Protocols*}
+section{*Theory of Agents and Messages for Security Protocols*}

theory Message imports Main begin
ML_file "../../antiquote_setup.ML"
--- a/src/Doc/Tutorial/Types/Records.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Doc/Tutorial/Types/Records.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,5 +1,5 @@

+section {* Records \label{sec:records} *}

(*<*)
theory Records imports Main begin
--- a/src/FOL/FOL.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/FOL.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lawrence C Paulson and Markus Wenzel
*)

-header {* Classical first-order logic *}
+section {* Classical first-order logic *}

theory FOL
imports IFOL
--- a/src/FOL/IFOL.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/IFOL.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lawrence C Paulson and Markus Wenzel
*)

-header {* Intuitionistic first-order logic *}
+section {* Intuitionistic first-order logic *}

theory IFOL
imports Pure
--- a/src/FOL/ex/Classical.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Classical.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Classical Predicate Calculus Problems*}

theory Classical imports FOL begin

--- a/src/FOL/ex/First_Order_Logic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/First_Order_Logic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Munich
*)

-header {* A simple formulation of First-Order Logic *}
+section {* A simple formulation of First-Order Logic *}

theory First_Order_Logic imports Pure begin

--- a/src/FOL/ex/Foundation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Foundation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
+section "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"

theory Foundation
imports IFOL
--- a/src/FOL/ex/If.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/If.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: the 'if' example *}
+section {* First-Order Logic: the 'if' example *}

theory If imports FOL begin

--- a/src/FOL/ex/Intro.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Intro.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Derives some inference rules, illustrating the use of definitions.
*)

-header {* Examples for the manual Introduction to Isabelle'' *}
+section {* Examples for the manual Introduction to Isabelle'' *}

theory Intro
imports FOL
--- a/src/FOL/ex/Intuitionistic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Intuitionistic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Intuitionistic First-Order Logic *}
+section {* Intuitionistic First-Order Logic *}

theory Intuitionistic
imports IFOL
--- a/src/FOL/ex/Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+section {* Theory of the natural numbers: Peano's axioms, primitive recursion *}

theory Nat
imports FOL
--- a/src/FOL/ex/Natural_Numbers.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Munich
*)

+section {* Natural numbers *}

theory Natural_Numbers
imports FOL
--- a/src/FOL/ex/Prolog.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Prolog.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: PROLOG examples *}
+section {* First-Order Logic: PROLOG examples *}

theory Prolog
imports FOL
--- a/src/FOL/ex/Propositional_Cla.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Propositional_Cla.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: propositional examples (classical version) *}
+section {* First-Order Logic: propositional examples (classical version) *}

theory Propositional_Cla
imports FOL
--- a/src/FOL/ex/Propositional_Int.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Propositional_Int.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: propositional examples (intuitionistic version) *}
+section {* First-Order Logic: propositional examples (intuitionistic version) *}

theory Propositional_Int
imports IFOL
--- a/src/FOL/ex/Quantifiers_Cla.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Quantifiers_Cla.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: quantifier examples (classical version) *}
+section {* First-Order Logic: quantifier examples (classical version) *}

theory Quantifiers_Cla
imports FOL
--- a/src/FOL/ex/Quantifiers_Int.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOL/ex/Quantifiers_Int.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: quantifier examples (intuitionistic version) *}
+section {* First-Order Logic: quantifier examples (intuitionistic version) *}

theory Quantifiers_Int
imports IFOL
--- a/src/FOLP/FOLP.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/FOLP.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Classical First-Order Logic with Proofs *}
+section {* Classical First-Order Logic with Proofs *}

theory FOLP
imports IFOLP
--- a/src/FOLP/IFOLP.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/IFOLP.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Intuitionistic First-Order Logic with Proofs *}
+section {* Intuitionistic First-Order Logic with Proofs *}

theory IFOLP
imports Pure
--- a/src/FOLP/ex/Foundation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/ex/Foundation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
+section "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"

theory Foundation
imports IFOLP
--- a/src/FOLP/ex/Intro.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/ex/Intro.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Derives some inference rules, illustrating the use of definitions.
*)

-header {* Examples for the manual Introduction to Isabelle'' *}
+section {* Examples for the manual Introduction to Isabelle'' *}

theory Intro
imports FOLP
--- a/src/FOLP/ex/Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/ex/Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+section {* Theory of the natural numbers: Peano's axioms, primitive recursion *}

theory Nat
imports FOLP
--- a/src/FOLP/ex/Propositional_Cla.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/ex/Propositional_Cla.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: propositional examples *}
+section {* First-Order Logic: propositional examples *}

theory Propositional_Cla
imports FOLP
--- a/src/FOLP/ex/Propositional_Int.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/FOLP/ex/Propositional_Int.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* First-Order Logic: propositional examples *}
+section {* First-Order Logic: propositional examples *}

theory Propositional_Int
imports IFOLP
--- a/src/HOL/ATP.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ATP.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

-header {* Automatic Theorem Provers (ATPs) *}
+section {* Automatic Theorem Provers (ATPs) *}

theory ATP
imports Meson
--- a/src/HOL/Algebra/Divisibility.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Stephan Hohe
*)

-header {* Divisibility in monoids and rings *}
+section {* Divisibility in monoids and rings *}

theory Divisibility
imports "~~/src/HOL/Library/Permutation" Coset Group
--- a/src/HOL/Archimedean_Field.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Archimedean_Field.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman
*)

-header {* Archimedean Fields, Floor and Ceiling Functions *}
+section {* Archimedean Fields, Floor and Ceiling Functions *}

theory Archimedean_Field
imports Main
--- a/src/HOL/Auth/Auth_Public.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Auth_Public.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}
+section {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}

theory Auth_Public
imports
--- a/src/HOL/Auth/Auth_Shared.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Auth_Shared.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
+section {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}

theory Auth_Shared
imports
--- a/src/HOL/Auth/CertifiedEmail.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/CertifiedEmail.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
*)

+section{*The Certified Electronic Mail Protocol by Abadi et al.*}

theory CertifiedEmail imports Public begin

--- a/src/HOL/Auth/Event.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Event.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
stores are visible to him
*)

-header{*Theory of Events for Security Protocols*}
+section{*Theory of Events for Security Protocols*}

theory Event imports Message begin

--- a/src/HOL/Auth/Guard/Analz.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Decomposition of Analz into two parts*}
+section{*Decomposition of Analz into two parts*}

theory Analz imports Extensions begin

--- a/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Blanqui's "guard" concept: protocol-independent secrecy *}
+section {* Blanqui's "guard" concept: protocol-independent secrecy *}

theory Auth_Guard_Public
imports
--- a/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Blanqui's "guard" concept: protocol-independent secrecy *}
+section {* Blanqui's "guard" concept: protocol-independent secrecy *}

theory Auth_Guard_Shared
imports
--- a/src/HOL/Auth/Guard/Extensions.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {*Extensions to Standard Theories*}

theory Extensions
imports "../Event"
--- a/src/HOL/Auth/Guard/Guard.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Protocol-Independent Confidentiality Theorem on Nonces*}

theory Guard imports Analz Extensions begin

--- a/src/HOL/Auth/Guard/GuardK.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
- the hypothesis Key n ~:G (keyset G) is added
*)

+section{*protocol-independent confidentiality theorem on keys*}

theory GuardK
imports Analz Extensions
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Incorporating Lowe's fix (inclusion of B's identity in round 2).
*)

+section{*Needham-Schroeder-Lowe Public-Key Protocol*}

theory Guard_NS_Public imports Guard_Public begin

--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Otway-Rees Protocol*}

theory Guard_OtwayRees imports Guard_Shared begin

--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*lemmas on guarded messages for protocols with symmetric keys*}
+section{*lemmas on guarded messages for protocols with symmetric keys*}

theory Guard_Shared imports Guard GuardK "../Shared" begin

--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Yahalom Protocol*}

theory Guard_Yahalom imports "../Shared" Guard_Shared begin

--- a/src/HOL/Auth/Guard/List_Msg.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Lists of Messages and Lists of Agents*}
+section{*Lists of Messages and Lists of Agents*}

theory List_Msg imports Extensions begin

--- a/src/HOL/Auth/Guard/P1.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/P1.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Mobiles Agents 1998, LNCS 1477.
*)

+section{*Protocol P1*}

theory P1 imports "../Public" Guard_Public List_Msg begin

--- a/src/HOL/Auth/Guard/P2.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/P2.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Mobiles Agents 1998, LNCS 1477.
*)

+section{*Protocol P2*}

theory P2 imports Guard_Public List_Msg begin

--- a/src/HOL/Auth/Guard/Proto.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Other Protocol-Independent Results*}

theory Proto imports Guard_Public begin

--- a/src/HOL/Auth/KerberosIV.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/KerberosIV.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Kerberos Protocol, Version IV*}

theory KerberosIV imports Public begin

--- a/src/HOL/Auth/KerberosIV_Gets.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Kerberos Protocol, Version IV*}

theory KerberosIV_Gets imports Public begin

--- a/src/HOL/Auth/KerberosV.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/KerberosV.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Giampaolo Bella, Catania University
*)

+section{*The Kerberos Protocol, Version V*}

theory KerberosV imports Public begin

--- a/src/HOL/Auth/Kerberos_BAN.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Kerberos Protocol, BAN Version*}

theory Kerberos_BAN imports Public begin

--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Giampaolo Bella, Catania University
*)

-header{*The Kerberos Protocol, BAN Version, with Gets event*}
+section{*The Kerberos Protocol, BAN Version, with Gets event*}

theory Kerberos_BAN_Gets imports Public begin

--- a/src/HOL/Auth/Message.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Message.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Inductive relations "parts", "analz" and "synth"
*)

-header{*Theory of Agents and Messages for Security Protocols*}
+section{*Theory of Agents and Messages for Security Protocols*}

theory Message
imports Main
--- a/src/HOL/Auth/NS_Public.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/NS_Public.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Version incorporating Lowe's fix (inclusion of B's identity in round 2).
*)

+section{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*}

theory NS_Public imports Public begin

--- a/src/HOL/Auth/NS_Public_Bad.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -10,7 +10,7 @@
Proc. Royal Soc. 426 (1989)
*)

+section{*Verifying the Needham-Schroeder Public-Key Protocol*}


--- a/src/HOL/Auth/NS_Shared.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/NS_Shared.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
+section{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}

theory NS_Shared imports Public begin

--- a/src/HOL/Auth/OtwayRees.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Original Otway-Rees Protocol*}

theory OtwayRees imports Public begin

--- a/src/HOL/Auth/OtwayReesBella.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Giampaolo Bella, Catania University
*)

-header{*Bella's version of the Otway-Rees protocol*}
+section{*Bella's version of the Otway-Rees protocol*}

theory OtwayReesBella imports Public begin
--- a/src/HOL/Auth/OtwayRees_AN.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Otway-Rees Protocol as Modified by Abadi and Needham*}

theory OtwayRees_AN imports Public begin

--- a/src/HOL/Auth/OtwayRees_Bad.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
*)

-header{*The Otway-Rees Protocol: The Faulty BAN Version*}
+section{*The Otway-Rees Protocol: The Faulty BAN Version*}


--- a/src/HOL/Auth/Recur.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Recur.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Otway-Bull Recursive Authentication Protocol*}

theory Recur imports Public begin

--- a/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
+section {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}

theory Auth_Smartcard
imports
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header{*Theory of Events for Security Protocols that use smartcards*}
+section{*Theory of Events for Security Protocols that use smartcards*}

theory EventSC
imports
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@
(*  Author:     Giampaolo Bella, Catania University
*)

+section{*Original Shoup-Rubin protocol*}

theory ShoupRubin imports Smartcard begin

--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@
(*  Author:     Giampaolo Bella, Catania University
*)

-header{*Bella's modification of the Shoup-Rubin protocol*}
+section{*Bella's modification of the Shoup-Rubin protocol*}

theory ShoupRubinBella imports Smartcard begin

--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@
(* Author:     Giampaolo Bella, Catania University
*)

+section{*Theory of smartcards*}

theory Smartcard
imports EventSC "../All_Symmetric"
--- a/src/HOL/Auth/TLS.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/TLS.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -38,7 +38,7 @@
Notes A {|Agent B, Nonce PMS|}.
*)

-header{*The TLS Protocol: Transport Layer Security*}
+section{*The TLS Protocol: Transport Layer Security*}

theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin

--- a/src/HOL/Auth/WooLam.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/WooLam.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Woo-Lam Protocol*}

theory WooLam imports Public begin

--- a/src/HOL/Auth/Yahalom.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Yahalom Protocol*}

theory Yahalom imports Public begin

--- a/src/HOL/Auth/Yahalom2.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Yahalom2.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The Yahalom Protocol, Variant 2*}

theory Yahalom2 imports Public begin

--- a/src/HOL/Auth/Yahalom_Bad.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*The Yahalom Protocol: A Flawed Version*}
+section{*The Yahalom Protocol: A Flawed Version*}


--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Cardinal arithmetic as needed by bounded natural functors.
*)

-header {* Cardinal Arithmetic as Needed by Bounded Natural Functors *}
+section {* Cardinal Arithmetic as Needed by Bounded Natural Functors *}

theory BNF_Cardinal_Arithmetic
imports BNF_Cardinal_Order_Relation
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Cardinal-order relations as needed by bounded natural functors.
*)

-header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
+section {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}

theory BNF_Cardinal_Order_Relation
imports Zorn BNF_Wellorder_Constructions
--- a/src/HOL/BNF_Composition.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Composition.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Composition of bounded natural functors.
*)

-header {* Composition of Bounded Natural Functors *}
+section {* Composition of Bounded Natural Functors *}

theory BNF_Composition
imports BNF_Def
--- a/src/HOL/BNF_Def.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Definition of bounded natural functors.
*)

-header {* Definition of Bounded Natural Functors *}
+section {* Definition of Bounded Natural Functors *}

theory BNF_Def
imports BNF_Cardinal_Arithmetic Fun_Def_Base
--- a/src/HOL/BNF_Fixpoint_Base.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
Shared fixpoint operations on bounded natural functors.
*)

-header {* Shared Fixpoint Operations on Bounded Natural Functors *}
+section {* Shared Fixpoint Operations on Bounded Natural Functors *}

theory BNF_Fixpoint_Base
imports BNF_Composition Basic_BNFs
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Greatest fixpoint (codatatype) operation on bounded natural functors.
*)

-header {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *}
+section {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *}

theory BNF_Greatest_Fixpoint
imports BNF_Fixpoint_Base String
--- a/src/HOL/BNF_Least_Fixpoint.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Least fixpoint (datatype) operation on bounded natural functors.
*)

-header {* Least Fixpoint (Datatype) Operation on Bounded Natural Functors *}
+section {* Least Fixpoint (Datatype) Operation on Bounded Natural Functors *}

theory BNF_Least_Fixpoint
imports BNF_Fixpoint_Base
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Constructions on wellorders as needed by bounded natural functors.
*)

-header {* Constructions on Wellorders as Needed by Bounded Natural Functors *}
+section {* Constructions on Wellorders as Needed by Bounded Natural Functors *}

theory BNF_Wellorder_Constructions
imports BNF_Wellorder_Embedding
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Well-order embeddings as needed by bounded natural functors.
*)

-header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
+section {* Well-Order Embeddings as Needed by Bounded Natural Functors *}

theory BNF_Wellorder_Embedding
imports Hilbert_Choice BNF_Wellorder_Relation
--- a/src/HOL/BNF_Wellorder_Relation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Well-order relations as needed by bounded natural functors.
*)

-header {* Well-Order Relations as Needed by Bounded Natural Functors *}
+section {* Well-Order Relations as Needed by Bounded Natural Functors *}

theory BNF_Wellorder_Relation
imports Order_Relation
--- a/src/HOL/Basic_BNFs.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Registration of basic types as bounded natural functors.
*)

-header {* Registration of Basic Types as Bounded Natural Functors *}
+section {* Registration of Basic Types as Bounded Natural Functors *}

theory Basic_BNFs
imports BNF_Def
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Cardinal arithmetic.
*)

+section {* Cardinal Arithmetic *}

theory Cardinal_Arithmetic
imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Cardinal-order relations.
*)

+section {* Cardinal-Order Relations *}

theory Cardinal_Order_Relation
imports BNF_Cardinal_Order_Relation Wellorder_Constructions
--- a/src/HOL/Cardinals/Cardinals.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Cardinals.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Theory of ordinals and cardinals.
*)

-header {* Theory of Ordinals and Cardinals *}
+section {* Theory of Ordinals and Cardinals *}

theory Cardinals
imports Ordinal_Arithmetic Cardinal_Arithmetic Wellorder_Extension
--- a/src/HOL/Cardinals/Fun_More.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
More on injections, bijections and inverses.
*)

-header {* More on Injections, Bijections and Inverses *}
+section {* More on Injections, Bijections and Inverses *}

theory Fun_More
imports Main
--- a/src/HOL/Cardinals/Order_Relation_More.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Basics on order-like relations.
*)

-header {* Basics on Order-Like Relations *}
+section {* Basics on Order-Like Relations *}

theory Order_Relation_More
imports Main
--- a/src/HOL/Cardinals/Order_Union.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
The ordinal-like sum of two orders with disjoint fields
*)

+section {* Order Union *}

theory Order_Union
imports Order_Relation
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Ordinal arithmetic.
*)

+section {* Ordinal Arithmetic *}

theory Ordinal_Arithmetic
imports Wellorder_Constructions
--- a/src/HOL/Cardinals/Wellfounded_More.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
More on well-founded relations.
*)

-header {* More on Well-Founded Relations *}
+section {* More on Well-Founded Relations *}

theory Wellfounded_More
imports Wellfounded Order_Relation_More
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Constructions on wellorders.
*)

-header {* Constructions on Wellorders *}
+section {* Constructions on Wellorders *}

theory Wellorder_Constructions
imports
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Well-order embeddings.
*)

+section {* Well-Order Embeddings *}

theory Wellorder_Embedding
imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation
--- a/src/HOL/Cardinals/Wellorder_Extension.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Christian Sternagel, JAIST
*)

-header {* Extending Well-founded Relations to Wellorders *}
+section {* Extending Well-founded Relations to Wellorders *}

theory Wellorder_Extension
imports Main Order_Union
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Well-order relations.
*)

+section {* Well-Order Relations *}

theory Wellorder_Relation
imports BNF_Wellorder_Relation Wellfounded_More
--- a/src/HOL/Code_Evaluation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Code_Evaluation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Florian Haftmann, TU Muenchen
*)

-header {* Term evaluation using the generic code generator *}
+section {* Term evaluation using the generic code generator *}

theory Code_Evaluation
imports Typerep Limited_Sequence
--- a/src/HOL/Code_Numeral.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Florian Haftmann, TU Muenchen
*)

-header {* Numeric types for code generation onto target language numerals only *}
+section {* Numeric types for code generation onto target language numerals only *}

theory Code_Numeral
imports Nat_Transfer Divides Lifting
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Florian Haftmann, TU Muenchen *)

-header {* A huge collection of equations to generate code from *}
+section {* A huge collection of equations to generate code from *}

theory Candidates
imports
--- a/src/HOL/Codegenerator_Test/Generate.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Florian Haftmann, TU Muenchen *)

-header {* Pervasive test of code generator *}
+section {* Pervasive test of code generator *}

theory Generate
imports
--- a/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Florian Haftmann, TU Muenchen *)

-header {* Pervasive test of code generator *}
+section {* Pervasive test of code generator *}

theory Generate_Binary_Nat
imports
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Ondrej Kuncar, TU Muenchen *)

-header {* Pervasive test of code generator *}
+section {* Pervasive test of code generator *}

theory Generate_Efficient_Datastructures
imports
--- a/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Florian Haftmann, TU Muenchen *)

-header {* Pervasive test of code generator *}
+section {* Pervasive test of code generator *}

theory Generate_Pretty_Char
imports
--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Florian Haftmann, TU Muenchen *)

-header {* Pervasive test of code generator *}
+section {* Pervasive test of code generator *}

theory Generate_Target_Nat
imports
--- a/src/HOL/Coinduction.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Coinduction.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Coinduction method that avoids some boilerplate compared to coinduct.
*)

+section {* Coinduction Method *}

theory Coinduction
imports Ctr_Sugar
--- a/src/HOL/Complete_Lattices.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)

+section {* Complete lattices *}

theory Complete_Lattices
imports Fun
--- a/src/HOL/Complete_Partial_Order.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Complete_Partial_Order.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:   Alexander Krauss, TU Muenchen
*)

-header {* Chain-complete partial orders and their fixpoints *}
+section {* Chain-complete partial orders and their fixpoints *}

theory Complete_Partial_Order
imports Product_Type
--- a/src/HOL/Complex.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Complex.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)

-header {* Complex Numbers: Rectangular and Polar Representations *}
+section {* Complex Numbers: Rectangular and Polar Representations *}

theory Complex
imports Transcendental
--- a/src/HOL/Complex_Main.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Complex_Main.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* Comprehensive Complex Theory *}
+section {* Comprehensive Complex Theory *}

theory Complex_Main
imports
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Luke S. Serafin, Carnegie Mellon University
*)

+section {* Conditionally-complete Lattices *}

theory Conditionally_Complete_Lattices
imports Main
--- a/src/HOL/Ctr_Sugar.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Ctr_Sugar.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Wrapping existing freely generated type's constructors.
*)

-header {* Wrapping Existing Freely Generated Type's Constructors *}
+section {* Wrapping Existing Freely Generated Type's Constructors *}

theory Ctr_Sugar
imports HOL
--- a/src/HOL/Datatype_Examples/Compat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Compat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Tests for compatibility with the old datatype package.
*)

-header {* Tests for Compatibility with the Old Datatype Package *}
+section {* Tests for Compatibility with the Old Datatype Package *}

theory Compat
imports "~~/src/HOL/Library/Old_Datatype"
--- a/src/HOL/Datatype_Examples/Derivation_Trees/DTree.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/DTree.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Derivation trees with nonterminal internal nodes and terminal leaves.
*)

-header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *}
+section {* Trees with Nonterminal Internal Nodes and Terminal Leaves *}

theory DTree
imports Prelim
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Language of a grammar.
*)

-header {* Language of a Grammar *}
+section {* Language of a Grammar *}

theory Gram_Lang
imports DTree "~~/src/HOL/Library/Infinite_Set"
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Parallel.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Parallel.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Parallel composition.
*)

+section {* Parallel Composition *}

theory Parallel
imports DTree
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Preliminaries.
*)

+section {* Preliminaries *}

theory Prelim
imports "~~/src/HOL/Library/FSet"
--- a/src/HOL/Datatype_Examples/IsaFoR.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/IsaFoR.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Benchmark consisting of datatypes defined in IsaFoR.
*)

-header {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
+section {* Benchmark Consisting of Datatypes Defined in IsaFoR *}

theory IsaFoR
imports Real
--- a/src/HOL/Datatype_Examples/Koenig.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Koenig.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Koenig's lemma.
*)

+section {* Koenig's Lemma *}

theory Koenig
imports TreeFI "~~/src/HOL/Library/Stream"
--- a/src/HOL/Datatype_Examples/Lambda_Term.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Lambda_Term.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Lambda-terms.
*)

+section {* Lambda-Terms *}

theory Lambda_Term
imports "~~/src/HOL/Library/FSet"
--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Miscellaneous codatatype definitions.
*)

-header {* Miscellaneous Codatatype Definitions *}
+section {* Miscellaneous Codatatype Definitions *}

theory Misc_Codatatype
imports "~~/src/HOL/Library/FSet"
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Miscellaneous datatype definitions.
*)

-header {* Miscellaneous Datatype Definitions *}
+section {* Miscellaneous Datatype Definitions *}

theory Misc_Datatype
imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet"
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Misc_N2M.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Miscellaneous tests for the nested-to-mutual reduction.
*)

-header \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
+section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>

theory Misc_N2M
imports "~~/src/HOL/Library/BNF_Axiomatization"
--- a/src/HOL/Datatype_Examples/Misc_Primcorec.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Primcorec.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Miscellaneous primitive corecursive function definitions.
*)

-header {* Miscellaneous Primitive Corecursive Function Definitions *}
+section {* Miscellaneous Primitive Corecursive Function Definitions *}

theory Misc_Primcorec
imports Misc_Codatatype
--- a/src/HOL/Datatype_Examples/Misc_Primrec.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Primrec.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Miscellaneous primitive recursive function definitions.
*)

-header {* Miscellaneous Primitive Recursive Function Definitions *}
+section {* Miscellaneous Primitive Recursive Function Definitions *}

theory Misc_Primrec
imports Misc_Datatype
--- a/src/HOL/Datatype_Examples/Process.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Process.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Processes.
*)

+section {* Processes *}

theory Process
imports "~~/src/HOL/Library/Stream"
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Stream processors---a syntactic representation of continuous functions on streams.
*)

-header {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
+section {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}

theory Stream_Processor
imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
--- a/src/HOL/Datatype_Examples/TreeFI.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/TreeFI.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Finitely branching possibly infinite trees.
*)

-header {* Finitely Branching Possibly Infinite Trees *}
+section {* Finitely Branching Possibly Infinite Trees *}

theory TreeFI
imports Main
--- a/src/HOL/Datatype_Examples/TreeFsetI.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Datatype_Examples/TreeFsetI.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Finitely branching possibly infinite trees, with sets of children.
*)

-header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
+section {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}

theory TreeFsetI
imports "~~/src/HOL/Library/FSet"
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@
(* Author:     Johannes Hoelzl, TU Muenchen
Coercions removed by Dmitriy Traytel *)

-header {* Prove Real Valued Inequalities by Computation *}
+section {* Prove Real Valued Inequalities by Computation *}

theory Approximation
imports
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Proving equalities in commutative rings done "right" in Isabelle/HOL.
*)

-header {* Proving equalities in commutative rings *}
+section {* Proving equalities in commutative rings *}

theory Commutative_Ring
imports Main
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
in normal form, the cring method is complete.
*)

-header {* Proof of the relative completeness of method comm-ring *}
+section {* Proof of the relative completeness of method comm-ring *}

theory Commutative_Ring_Complete
imports Commutative_Ring
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author      : Amine Chaieb, TU Muenchen
*)

-header {* Dense linear order without endpoints
+section {* Dense linear order without endpoints
and a quantifier elimination procedure in Ferrante and Rackoff style *}

theory Dense_Linear_Order
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
+section{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}

theory Parametric_Ferrante_Rackoff
imports
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-header {* Univariate Polynomials as lists *}
+section {* Univariate Polynomials as lists *}

theory Polynomial_List
imports Complex_Main
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-header {* Rational numbers as pairs *}
+section {* Rational numbers as pairs *}

theory Rat_Pair
imports Complex_Main
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-header {* Implementation and verification of multivariate polynomials *}
+section {* Implementation and verification of multivariate polynomials *}

theory Reflected_Multivariate_Polynomial
imports Complex_Main Rat_Pair Polynomial_List
--- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Author:     Bernhard Haeupler *)

-header {* Some examples demonstrating the comm-ring method *}
+section {* Some examples demonstrating the comm-ring method *}

theory Commutative_Ring_Ex
imports "../Commutative_Ring"
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author:     Amine Chaieb, TU Muenchen *)

-header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
+section {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}

theory Dense_Linear_Order_Ex
imports "../Dense_Linear_Order"
--- a/src/HOL/Deriv.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Deriv.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
GMVT by Benjamin Porter, 2005
*)

+section{* Differentiation *}

theory Deriv
imports Limits
--- a/src/HOL/Divides.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Divides.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The division operators div and mod *}
+section {* The division operators div and mod *}

theory Divides
imports Parity
--- a/src/HOL/Enum.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Enum.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)

-header {* Finite types as explicit enumerations *}
+section {* Finite types as explicit enumerations *}

theory Enum
imports Map Groups_List
--- a/src/HOL/Equiv_Relations.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Equivalence Relations in Higher-Order Set Theory *}
+section {* Equivalence Relations in Higher-Order Set Theory *}

theory Equiv_Relations
imports Groups_Big Relation
--- a/src/HOL/Extraction.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Extraction.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

-header {* Program extraction for HOL *}
+section {* Program extraction for HOL *}

theory Extraction
imports Option
--- a/src/HOL/Fact.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Fact.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
*)

+section{*Factorial Function*}

theory Fact
imports Main
--- a/src/HOL/Fields.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Fields.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
*)

+section {* Fields *}

theory Fields
imports Rings
--- a/src/HOL/Finite_Set.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
with contributions by Jeremy Avigad and Andrei Popescu
*)

+section {* Finite sets *}

theory Finite_Set
imports Product_Type Sum_Type Nat
--- a/src/HOL/Fun.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Fun.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
*)

+section {* Notions about functions *}

theory Fun
imports Set
--- a/src/HOL/Fun_Def.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Fun_Def.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Alexander Krauss, TU Muenchen
*)

-header {* Function Definitions and Termination Proofs *}
+section {* Function Definitions and Termination Proofs *}

theory Fun_Def
imports Basic_BNF_Least_Fixpoints Partial_Function SAT
--- a/src/HOL/Fun_Def_Base.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Fun_Def_Base.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Alexander Krauss, TU Muenchen
*)

-header {* Function Definition Base *}
+section {* Function Definition Base *}

theory Fun_Def_Base
imports Ctr_Sugar Set Wellfounded
--- a/src/HOL/GCD.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/GCD.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -25,7 +25,7 @@
*)

-header {* Greatest common divisor and least common multiple *}
+section {* Greatest common divisor and least common multiple *}

theory GCD
imports Fact
--- a/src/HOL/Groebner_Basis.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, TU Muenchen
*)

+section {* Groebner bases *}

theory Groebner_Basis
imports Semiring_Normalization Parity
--- a/src/HOL/Groups.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Groups.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
*)

-header {* Groups, also combined with orderings *}
+section {* Groups, also combined with orderings *}

theory Groups
imports Orderings
--- a/src/HOL/Groups_Big.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Groups_Big.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Big sum and product over finite (non-empty) sets *}
+section {* Big sum and product over finite (non-empty) sets *}

theory Groups_Big
imports Finite_Set
--- a/src/HOL/Groups_List.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Groups_List.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Tobias Nipkow, TU Muenchen *)

-header {* Sum and product over lists *}
+section {* Sum and product over lists *}

theory Groups_List
imports List
--- a/src/HOL/HOL.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/HOL.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
*)

-header {* The basis of Higher-Order Logic *}
+section {* The basis of Higher-Order Logic *}

theory HOL
imports Pure "~~/src/Tools/Code_Generator"
--- a/src/HOL/Hahn_Banach/Bounds.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Bounds.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Bounds\<close>

theory Bounds
imports Main "~~/src/HOL/Library/ContNotDenum"
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

-header \<open>The norm of a function\<close>
+section \<open>The norm of a function\<close>

theory Function_Norm
imports Normed_Space Function_Order
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>An order on functions\<close>

theory Function_Order
imports Subspace Linearform
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>The Hahn-Banach Theorem\<close>

theory Hahn_Banach
imports Hahn_Banach_Lemmas
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Extending non-maximal functions\<close>

theory Hahn_Banach_Ext_Lemmas
imports Function_Norm
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

-header \<open>The supremum w.r.t.~the function order\<close>
+section \<open>The supremum w.r.t.~the function order\<close>

theory Hahn_Banach_Sup_Lemmas
imports Function_Norm Zorn_Lemma
--- a/src/HOL/Hahn_Banach/Linearform.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Linearform.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Linearforms\<close>

theory Linearform
imports Vector_Space
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Normed vector spaces\<close>

theory Normed_Space
imports Subspace
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Subspaces\<close>

theory Subspace
imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Vector spaces\<close>

theory Vector_Space
imports Complex_Main Bounds
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer, TU Munich
*)

+section \<open>Zorn's Lemma\<close>

theory Zorn_Lemma
imports Main
--- a/src/HOL/Hilbert_Choice.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
+section {* Hilbert's Epsilon-Operator and the Axiom of Choice *}

theory Hilbert_Choice
imports Nat Wellfounded
--- a/src/HOL/IMP/AExp.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/AExp.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "Arithmetic and Boolean Expressions"

theory AExp imports Main begin

--- a/src/HOL/IMP/ASM.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/ASM.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "Stack Machine and Compilation"

theory ASM imports AExp begin

--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)

+section "Denotational Abstract Interpretation"

theory Abs_Int_den0_fun
imports "~~/src/Tools/Permanent_Interpretation" "../Big_Step"
--- a/src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)

+section "Abstract Interpretation (ITP)"

theory Complete_Lattice_ix
imports Main
--- a/src/HOL/IMP/Com.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Com.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header "IMP --- A Simple Imperative Language"
+section "IMP --- A Simple Imperative Language"

theory Com imports BExp begin

--- a/src/HOL/IMP/Compiler.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Compiler.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow and Gerwin Klein *)

+section "Compiler for IMP"

theory Compiler imports Big_Step Star
begin
--- a/src/HOL/IMP/Complete_Lattice.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Complete_Lattice.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "Abstract Interpretation"

theory Complete_Lattice
imports Main
--- a/src/HOL/IMP/Denotational.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Denotational.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)

+section "Denotational Semantics of Commands"

theory Denotational imports Big_Step begin

--- a/src/HOL/IMP/Hoare.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Hoare.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)

+section "Hoare Logic"

theory Hoare imports Big_Step begin

--- a/src/HOL/IMP/Live.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Live.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)

+section "Live Variable Analysis"

theory Live imports Vars Big_Step
begin
--- a/src/HOL/IMP/Procs.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Procs.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header "Extensions and Variations of IMP"
+section "Extensions and Variations of IMP"

theory Procs imports BExp begin

--- a/src/HOL/IMP/Sec_Type_Expr.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "Security Type Systems"

theory Sec_Type_Expr imports Big_Step
begin
--- a/src/HOL/IMP/Sem_Equiv.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Sem_Equiv.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "Constant Folding"

theory Sem_Equiv
imports Big_Step
--- a/src/HOL/IMP/Small_Step.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Small_Step.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "Small-Step Semantics of Commands"

theory Small_Step imports Star Big_Step begin

--- a/src/HOL/IMP/Types.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Types.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section "A Typed Language"

theory Types imports Star Complex_Main begin

--- a/src/HOL/IMP/Vars.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMP/Vars.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)

+section "Definite Initialization Analysis"

theory Vars imports Com
begin
--- a/src/HOL/IMPP/Com.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMPP/Com.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
*)

-header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
+section {* Semantics of arithmetic and boolean expressions, Syntax of commands *}

theory Com
imports Main
--- a/src/HOL/IMPP/EvenOdd.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     David von Oheimb, TUM
*)

-header {* Example of mutually recursive procedures verified with Hoare logic *}
+section {* Example of mutually recursive procedures verified with Hoare logic *}

theory EvenOdd
imports Main Misc
--- a/src/HOL/IMPP/Hoare.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Inductive definition of Hoare logic for partial correctness *}
+section {* Inductive definition of Hoare logic for partial correctness *}

theory Hoare
imports Natural
--- a/src/HOL/IMPP/Misc.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMPP/Misc.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     David von Oheimb, TUM
*)

-header {* Several examples for Hoare logic *}
+section {* Several examples for Hoare logic *}

theory Misc
imports Hoare
--- a/src/HOL/IMPP/Natural.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IMPP/Natural.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
*)

-header {* Natural semantics of commands *}
+section {* Natural semantics of commands *}

theory Natural
imports Com
--- a/src/HOL/IOA/Asig.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IOA/Asig.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Action signatures *}

theory Asig
imports Main
--- a/src/HOL/IOA/IOA.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IOA/IOA.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The I/O automata of Lynch and Tuttle *}
+section {* The I/O automata of Lynch and Tuttle *}

theory IOA
imports Asig
--- a/src/HOL/IOA/Solve.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/IOA/Solve.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Weak possibilities mapping (abstraction) *}
+section {* Weak possibilities mapping (abstraction) *}

theory Solve
imports IOA
--- a/src/HOL/Imperative_HOL/Array.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

theory Array
imports Heap_Monad
--- a/src/HOL/Imperative_HOL/Heap.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
*)

-header {* A polymorphic heap based on cantor encodings *}
+section {* A polymorphic heap based on cantor encodings *}

theory Heap
imports Main "~~/src/HOL/Library/Countable"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

-header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
+section {* A monad with a polymorphic heap and primitive reasoning infrastructure *}

imports
--- a/src/HOL/Imperative_HOL/Imperative_HOL.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

+section {* Entry point into monadic imperative HOL *}

theory Imperative_HOL
imports Array Ref
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

+section {* Monadic imperative HOL with examples *}

theory Imperative_HOL_ex
imports Imperative_HOL Overview
--- a/src/HOL/Imperative_HOL/Ref.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

theory Ref
imports Array
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

-header {* An imperative implementation of Quicksort on arrays *}
+section {* An imperative implementation of Quicksort on arrays *}

theory Imperative_Quicksort
imports
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

-header {* An imperative in-place reversal on arrays *}
+section {* An imperative in-place reversal on arrays *}

theory Imperative_Reverse
imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

+section {* Linked Lists by ML references *}

imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Target_Int"
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

-header {* An efficient checker for proofs from a SAT solver *}
+section {* An efficient checker for proofs from a SAT solver *}

theory SatChecker
imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL"
--- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

-header {* Sorted lists as representation of finite sets *}
+section {* Sorted lists as representation of finite sets *}

theory Sorted_List
imports Main
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

+section {* Theorems about sub arrays *}

theory Subarray
imports "~~/src/HOL/Imperative_HOL/Array" Sublist
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, TU Muenchen
*)

-header {* Slices of lists *}
+section {* Slices of lists *}

theory Sublist
imports "~~/src/HOL/Library/Multiset"
--- a/src/HOL/Import/HOL_Light_Import.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Import.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Alexander Krauss, QAware GmbH
*)

-header {* Main HOL Light importer *}
+section {* Main HOL Light importer *}

theory HOL_Light_Import
imports HOL_Light_Maps
--- a/src/HOL/Import/HOL_Light_Maps.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Based on earlier code by Steven Obua and Sebastian Skalberg
*)

-header {* Type and constant mappings of HOL Light importer *}
+section {* Type and constant mappings of HOL Light importer *}

theory HOL_Light_Maps
imports Import_Setup
--- a/src/HOL/Import/Import_Setup.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Import/Import_Setup.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Alexander Krauss, QAware GmbH
*)

-header {* Importer machinery and required theorems *}
+section {* Importer machinery and required theorems *}

theory Import_Setup
imports Main "~~/src/HOL/Fact"
--- a/src/HOL/Induct/ABexp.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/ABexp.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

-header {* Arithmetic and boolean expressions *}
+section {* Arithmetic and boolean expressions *}

theory ABexp
imports Main
--- a/src/HOL/Induct/Com.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Com.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)

-header{*Mutual Induction via Iteratived Inductive Definitions*}
+section{*Mutual Induction via Iteratived Inductive Definitions*}

theory Com imports Main begin

--- a/src/HOL/Induct/Comb.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Comb.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Combinatory Logic example: the Church-Rosser Theorem *}
+section {* Combinatory Logic example: the Church-Rosser Theorem *}

theory Comb imports Main begin

--- a/src/HOL/Induct/Common_Patterns.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Common_Patterns.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Makarius
*)

-header {* Common patterns of induction *}
+section {* Common patterns of induction *}

theory Common_Patterns
imports Main
--- a/src/HOL/Induct/Ordinals.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Ordinals.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
*)

+section {* Ordinals *}

theory Ordinals
imports Main
--- a/src/HOL/Induct/PropLog.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/PropLog.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Copyright   1994  TU Muenchen & University of Cambridge
*)

-header {* Meta-theory of propositional logic *}
+section {* Meta-theory of propositional logic *}

theory PropLog imports Main begin

--- a/src/HOL/Induct/QuoDataType.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Defining an Initial Algebra by Quotienting a Free Algebra*}
+section{*Defining an Initial Algebra by Quotienting a Free Algebra*}

theory QuoDataType imports Main begin

--- a/src/HOL/Induct/QuoNestedDataType.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Quotienting a Free Algebra Involving Nested Recursion*}
+section{*Quotienting a Free Algebra Involving Nested Recursion*}

theory QuoNestedDataType imports Main begin

--- a/src/HOL/Induct/SList.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/SList.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -21,7 +21,7 @@
datatype 'a m = Node 'a * 'a m list
*)

-header {* Extended List Theory (old) *}
+section {* Extended List Theory (old) *}

theory SList
imports Sexp
--- a/src/HOL/Induct/Sigma_Algebra.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Sigma_Algebra.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Muenchen
*)

+section {* Sigma algebras *}

theory Sigma_Algebra
imports Main
--- a/src/HOL/Induct/Term.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Term.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer,  TU Muenchen
*)

-header {* Terms over a given alphabet *}
+section {* Terms over a given alphabet *}

theory Term
imports Main
--- a/src/HOL/Induct/Tree.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Induct/Tree.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

-header {* Infinitely branching trees *}
+section {* Infinitely branching trees *}

theory Tree
imports Main
--- a/src/HOL/Inductive.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Inductive.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Muenchen
*)

-header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
+section {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}

theory Inductive
imports Complete_Lattices Ctr_Sugar
--- a/src/HOL/Int.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Int.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
*)

-header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
+section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}

theory Int
imports Equiv_Relations Power Quotient Fun_Def
--- a/src/HOL/Lattices.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lattices.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Tobias Nipkow
*)

+section {* Abstract lattices *}

theory Lattices
imports Groups
--- a/src/HOL/Lattices_Big.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lattices_Big.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
+section {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}

theory Lattices_Big
imports Finite_Set Option
--- a/src/HOL/Lazy_Sequence.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lazy_Sequence.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Lukas Bulwahn, TU Muenchen *)

+section {* Lazy sequences *}

theory Lazy_Sequence
imports Predicate
--- a/src/HOL/Lifting.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lifting.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Cezary Kaliszyk and Christian Urban
*)

+section {* Lifting package *}

theory Lifting
imports Equiv_Relations Transfer
--- a/src/HOL/Lifting_Option.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
*)

-header {* Setup for Lifting/Transfer for the option type *}
+section {* Setup for Lifting/Transfer for the option type *}

theory Lifting_Option
imports Lifting Option
--- a/src/HOL/Lifting_Product.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lifting_Product.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman and Ondrej Kuncar
*)

-header {* Setup for Lifting/Transfer for the product type *}
+section {* Setup for Lifting/Transfer for the product type *}

theory Lifting_Product
imports Lifting Basic_BNFs
--- a/src/HOL/Lifting_Set.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lifting_Set.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman and Ondrej Kuncar
*)

-header {* Setup for Lifting/Transfer for the set type *}
+section {* Setup for Lifting/Transfer for the set type *}

theory Lifting_Set
imports Lifting
--- a/src/HOL/Lifting_Sum.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman and Ondrej Kuncar
*)

-header {* Setup for Lifting/Transfer for the sum type *}
+section {* Setup for Lifting/Transfer for the sum type *}

theory Lifting_Sum
imports Lifting Basic_BNFs
--- a/src/HOL/Limited_Sequence.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Limited_Sequence.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Lukas Bulwahn, TU Muenchen *)

-header {* Depth-Limited Sequences with failure element *}
+section {* Depth-Limited Sequences with failure element *}

theory Limited_Sequence
imports Lazy_Sequence
--- a/src/HOL/Limits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Limits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
*)

-header {* Limits on Real Vector Spaces *}
+section {* Limits on Real Vector Spaces *}

theory Limits
imports Real_Vector_Spaces
--- a/src/HOL/List.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/List.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Tobias Nipkow
*)

-header {* The datatype of finite lists *}
+section {* The datatype of finite lists *}

theory List
imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
--- a/src/HOL/MacLaurin.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/MacLaurin.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard Häupler, 2005
*)

+section{*MacLaurin Series*}

theory MacLaurin
imports Transcendental
--- a/src/HOL/Main.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Main.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section {* Main HOL *}

theory Main
imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
--- a/src/HOL/Map.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Map.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
The datatype of maps' (written ~=>); strongly resembles maps in VDM.
*)

+section {* Maps *}

theory Map
imports List
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Steven Obua
*)

-header {* Floating Point Representation of the Reals *}
+section {* Floating Point Representation of the Reals *}

theory ComputeFloat
imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
--- a/src/HOL/Meson.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Meson.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
*)

-header {* MESON Proof Method *}
+section {* MESON Proof Method *}

theory Meson
imports Nat
--- a/src/HOL/Metis.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

-header {* Metis Proof Method *}
+section {* Metis Proof Method *}

theory Metis
imports ATP
--- a/src/HOL/Metis_Examples/Abstraction.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Example featuring Metis's support for lambda-abstractions.
*)

-header {* Example Featuring Metis's Support for Lambda-Abstractions *}
+section {* Example Featuring Metis's Support for Lambda-Abstractions *}

theory Abstraction
imports "~~/src/HOL/Library/FuncSet"
--- a/src/HOL/Metis_Examples/Big_O.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Metis example featuring the Big O notation.
*)

-header {* Metis Example Featuring the Big O Notation *}
+section {* Metis Example Featuring the Big O Notation *}

theory Big_O
imports
--- a/src/HOL/Metis_Examples/Binary_Tree.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Metis example featuring binary trees.
*)

-header {* Metis Example Featuring Binary Trees *}
+section {* Metis Example Featuring Binary Trees *}

theory Binary_Tree
imports Main
--- a/src/HOL/Metis_Examples/Clausification.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Example that exercises Metis's Clausifier.
*)

-header {* Example that Exercises Metis's Clausifier *}
+section {* Example that Exercises Metis's Clausifier *}

theory Clausification
imports Complex_Main
--- a/src/HOL/Metis_Examples/Message.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Metis example featuring message authentication.
*)

-header {* Metis Example Featuring Message Authentication *}
+section {* Metis Example Featuring Message Authentication *}

theory Message
imports Main
--- a/src/HOL/Metis_Examples/Proxies.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
rudimentary higher-order reasoning.
*)

+section {*
Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
Rudimentary Higher-Order Reasoning.
*}
--- a/src/HOL/Metis_Examples/Sets.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Metis example featuring typed set theory.
*)

-header {* Metis Example Featuring Typed Set Theory *}
+section {* Metis Example Featuring Typed Set Theory *}

theory Sets
imports Main
--- a/src/HOL/Metis_Examples/Tarski.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Metis example featuring the full theorem of Tarski.
*)

-header {* Metis Example Featuring the Full Theorem of Tarski *}
+section {* Metis Example Featuring the Full Theorem of Tarski *}

theory Tarski
imports Main "~~/src/HOL/Library/FuncSet"
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Metis example featuring the transitive closure.
*)

-header {* Metis Example Featuring the Transitive Closure *}
+section {* Metis Example Featuring the Transitive Closure *}

theory Trans_Closure
imports Main
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Example that exercises Metis's (and hence Sledgehammer's) type encodings.
*)

+section {*
Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings
*}

--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Sascha Boehme, TU Munich
*)

-header {* Simple test theory for Mirabelle actions *}
+section {* Simple test theory for Mirabelle actions *}

theory Mirabelle_Test
imports Main Mirabelle
--- a/src/HOL/NanoJava/AxSem.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     David von Oheimb, Technische Universitaet Muenchen
*)

+section "Axiomatic Semantics"

theory AxSem imports State begin

--- a/src/HOL/NanoJava/Decl.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/Decl.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header "Types, class Declarations, and whole programs"
+section "Types, class Declarations, and whole programs"

theory Decl imports Term begin

--- a/src/HOL/NanoJava/Equivalence.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header "Equivalence of Operational and Axiomatic Semantics"
+section "Equivalence of Operational and Axiomatic Semantics"

theory Equivalence imports OpSem AxSem begin

--- a/src/HOL/NanoJava/Example.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/Example.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section "Example"

theory Example
imports Equivalence
--- a/src/HOL/NanoJava/OpSem.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/OpSem.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section "Operational Evaluation Semantics"

theory OpSem imports State begin

--- a/src/HOL/NanoJava/State.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/State.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section "Program State"

theory State imports TypeRel begin

--- a/src/HOL/NanoJava/Term.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/Term.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     David von Oheimb, Technische Universitaet Muenchen
*)

+section "Statements and expression emulations"

theory Term imports Main begin

--- a/src/HOL/NanoJava/TypeRel.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     David von Oheimb, Technische Universitaet Muenchen
*)

+section "Type relations"

theory TypeRel
imports Decl
--- a/src/HOL/Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
and * (for div and mod, see theory Divides).
*)

+section {* Natural numbers *}

theory Nat
imports Inductive Typedef Fun Fields
--- a/src/HOL/Nat_Transfer.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nat_Transfer.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Authors: Jeremy Avigad and Amine Chaieb *)

-header {* Generic transfer machinery;  specific transfer from nats to ints and back. *}
+section {* Generic transfer machinery;  specific transfer from nats to ints and back. *}

theory Nat_Transfer
imports Int
--- a/src/HOL/Nitpick.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Nitpick: Yet another counterexample generator for Isabelle/HOL.
*)

-header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
+section {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}

theory Nitpick
imports Record
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick's functional core.
*)

-header {* Examples Featuring Nitpick's Functional Core *}
+section {* Examples Featuring Nitpick's Functional Core *}

theory Core_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick applied to datatypes.
*)

-header {* Examples Featuring Nitpick Applied to Datatypes *}
+section {* Examples Featuring Nitpick Applied to Datatypes *}

theory Datatype_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Nitpick example based on Tobias Nipkow's hotel key card formalization.
*)

-header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
+section {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
Formalization *}

theory Hotel_Nits
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick applied to (co)inductive definitions.
*)

-header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}
+section {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}

theory Induct_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick applied to natural numbers and integers.
*)

-header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
+section {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}

theory Integer_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples from the Nitpick manual.
*)

-header {* Examples from the Nitpick Manual *}
+section {* Examples from the Nitpick Manual *}

(* The "expect" arguments to Nitpick in this theory and the other example
theories are there so that the example can also serve as a regression test
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Minipick, the minimalistic version of Nitpick.
*)

-header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
+section {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}

theory Mini_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick's monotonicity check.
*)

-header {* Examples Featuring Nitpick's Monotonicity Check *}
+section {* Examples Featuring Nitpick's Monotonicity Check *}

theory Mono_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick's "destroy_constrs" optimization.
*)

-header {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}
+section {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}

theory Pattern_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick applied to records.
*)

-header {* Examples Featuring Nitpick Applied to Records *}
+section {* Examples Featuring Nitpick Applied to Records *}

theory Record_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
*)

+section {* Refute Examples Adapted to Nitpick *}

theory Refute_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick's "specialize" optimization.
*)

-header {* Examples Featuring Nitpick's \textit{specialize} Optimization *}
+section {* Examples Featuring Nitpick's \textit{specialize} Optimization *}

theory Special_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Nitpick tests.
*)

+section {* Nitpick Tests *}

theory Tests_Nits
imports Main
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Examples featuring Nitpick applied to typedefs.
*)

-header {* Examples Featuring Nitpick Applied to Typedefs *}
+section {* Examples Featuring Nitpick Applied to Typedefs *}

theory Typedef_Nits
imports Complex_Main
--- a/src/HOL/Nominal/Examples/Nominal_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Author:  Christian Urban TU Muenchen *)

-header {* Various examples involving nominal datatypes. *}
+section {* Various examples involving nominal datatypes. *}

theory Nominal_Examples
imports Nominal_Examples_Base Class3
--- a/src/HOL/Nominal/Examples/Nominal_Examples_Base.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nominal/Examples/Nominal_Examples_Base.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Author:  Christian Urban TU Muenchen *)

-header {* Various examples involving nominal datatypes. *}
+section {* Various examples involving nominal datatypes. *}

theory Nominal_Examples_Base
imports
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* Simply-typed lambda-calculus with let and tuple patterns *}
+section {* Simply-typed lambda-calculus with let and tuple patterns *}

theory Pattern
imports "../Nominal"
--- a/src/HOL/Nominal/Examples/Standardization.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Standardization *}

theory Standardization
imports "../Nominal"
--- a/src/HOL/NthRoot.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/NthRoot.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

-header {* Nth Roots of Real Numbers *}
+section {* Nth Roots of Real Numbers *}

theory NthRoot
imports Deriv
--- a/src/HOL/Num.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Num.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Brian Huffman
*)

+section {* Binary Numerals *}

theory Num
imports BNF_Least_Fixpoint
--- a/src/HOL/Number_Theory/Binomial.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Defines the "choose" function, and establishes basic properties.
*)

+section {* Binomial *}

theory Binomial
imports Cong Fact Complex_Main
--- a/src/HOL/Number_Theory/Cong.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -23,7 +23,7 @@
natural numbers and the integers, and added a number of new theorems.
*)

+section {* Congruence *}

theory Cong
imports Primes
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Florian Haftmann, TU Muenchen
*)

-header {* The sieve of Eratosthenes *}
+section {* The sieve of Eratosthenes *}

theory Eratosthenes
imports Main Primes
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Manuel Eberl *)

-header {* Abstract euclidean algorithm *}
+section {* Abstract euclidean algorithm *}

theory Euclidean_Algorithm
imports Complex_Main
--- a/src/HOL/Number_Theory/Fib.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Fib.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
*)

+section {* Fib *}

theory Fib
imports Binomial
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Ported by lcp but unfinished
*)

+section {* Gauss' Lemma *}

theory Gauss
imports Residues
--- a/src/HOL/Number_Theory/Number_Theory.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Number_Theory.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,5 +1,5 @@

-header {* Comprehensive number theory *}
+section {* Comprehensive number theory *}

theory Number_Theory
imports Fib Residues Eratosthenes
--- a/src/HOL/Number_Theory/Pocklington.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-header {* Pocklington's Theorem for Primes *}
+section {* Pocklington's Theorem for Primes *}

theory Pocklington
imports Residues
--- a/src/HOL/Number_Theory/Primes.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -25,7 +25,7 @@
*)

+section {* Primes *}

theory Primes
imports "~~/src/HOL/GCD"
--- a/src/HOL/Number_Theory/Residues.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Euler's theorem and Wilson's theorem.
*)

+section {* Residue rings *}

theory Residues
imports
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
that, by Jeremy Avigad and David Gray.
*)

+section {* UniqueFactorization *}

theory UniqueFactorization
imports Cong "~~/src/HOL/Library/Multiset"
--- a/src/HOL/Numeral_Simprocs.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Various *)

-header {* Combination and Cancellation Simprocs for Numeral Expressions *}
+section {* Combination and Cancellation Simprocs for Numeral Expressions *}

theory Numeral_Simprocs
imports Divides
--- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Bijections between sets *}
+section {* Bijections between sets *}

theory BijectionRel
imports Main
--- a/src/HOL/Old_Number_Theory/Chinese.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The Chinese Remainder Theorem *}
+section {* The Chinese Remainder Theorem *}

theory Chinese
imports IntPrimes
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

+section {* Euler's criterion *}

theory Euler
imports Residues EvenOdd
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Fermat's Little Theorem extended to Euler's Totient function *}
+section {* Fermat's Little Theorem extended to Euler's Totient function *}

theory EulerFermat
imports BijectionRel IntFact
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {*Parity: Even and Odd Integers*}
+section {*Parity: Even and Odd Integers*}

theory EvenOdd
imports Int2
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
+section {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}

theory Factorization
imports Primes "~~/src/HOL/Library/Permutation"
--- a/src/HOL/Old_Number_Theory/Fib.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Fib.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The Fibonacci function *}
+section {* The Fibonacci function *}

theory Fib
imports Primes
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {*Finite Sets and Finite Sums*}
+section {*Finite Sets and Finite Sums*}

theory Finite2
imports IntFact "~~/src/HOL/Library/Infinite_Set"
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

+section {* Gauss' Lemma *}

theory Gauss
imports Euler
--- a/src/HOL/Old_Number_Theory/Int2.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

+section {*Integers: Divisibility and Congruences*}

theory Int2
imports Finite2 WilsonRuss
--- a/src/HOL/Old_Number_Theory/IntFact.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/IntFact.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Factorial on integers *}
+section {* Factorial on integers *}

theory IntFact
imports IntPrimes
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Divisibility and prime numbers (on integers) *}
+section {* Divisibility and prime numbers (on integers) *}

theory IntPrimes
imports Primes
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The Greatest Common Divisor *}
+section {* The Greatest Common Divisor *}

theory Legacy_GCD
imports Main
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb
*)

-header {* Pocklington's Theorem for Primes *}
+section {* Pocklington's Theorem for Primes *}

theory Pocklington
imports Primes
--- a/src/HOL/Old_Number_Theory/Primes.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Primality on nat *}
+section {* Primality on nat *}

theory Primes
imports Complex_Main Legacy_GCD
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

+section {* The law of Quadratic reciprocity *}

imports Gauss
--- a/src/HOL/Old_Number_Theory/Residues.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

+section {* Residue Sets *}

theory Residues
imports Int2
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Wilson's Theorem using a more abstract approach *}
+section {* Wilson's Theorem using a more abstract approach *}

theory WilsonBij
imports BijectionRel IntFact
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Wilson's Theorem according to Russinoff *}
+section {* Wilson's Theorem according to Russinoff *}

theory WilsonRuss
imports EulerFermat
--- a/src/HOL/Option.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Option.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Folklore
*)

+section {* Datatype option *}

theory Option
imports BNF_Least_Fixpoint Finite_Set
--- a/src/HOL/Order_Relation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Order_Relation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Andrei Popescu, TU Muenchen
*)

-header {* Orders as Relations *}
+section {* Orders as Relations *}

theory Order_Relation
imports Wfrec
--- a/src/HOL/Orderings.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Orderings.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
*)

+section {* Abstract orderings *}

theory Orderings
imports HOL
--- a/src/HOL/Parity.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Parity.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Jacques D. Fleuriot
*)

-header {* Parity in rings and semirings *}
+section {* Parity in rings and semirings *}

theory Parity
imports Nat_Transfer
--- a/src/HOL/Partial_Function.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Partial_Function.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:   Alexander Krauss, TU Muenchen
*)

-header {* Partial Function Definitions *}
+section {* Partial Function Definitions *}

theory Partial_Function
imports Complete_Partial_Order Fun_Def_Base Option
--- a/src/HOL/Power.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Power.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Exponentiation *}

theory Power
imports Num Equiv_Relations
--- a/src/HOL/Predicate.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Predicate.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn and Florian Haftmann, TU Muenchen
*)

-header {* Predicates as enumerations *}
+section {* Predicates as enumerations *}

theory Predicate
imports String
--- a/src/HOL/Predicate_Compile.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Predicate_Compile.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
*)

-header {* A compiler for predicates defined by introduction rules *}
+section {* A compiler for predicates defined by introduction rules *}

theory Predicate_Compile
imports Random_Sequence Quickcheck_Exhaustive
--- a/src/HOL/Presburger.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Presburger.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, TU Muenchen
*)

-header {* Decision Procedure for Presburger Arithmetic *}
+section {* Decision Procedure for Presburger Arithmetic *}

theory Presburger
imports Groebner_Basis Set_Interval
--- a/src/HOL/Product_Type.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Product_Type.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Cartesian products *}

theory Product_Type
imports Typedef Inductive Fun
--- a/src/HOL/Prolog/Func.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Prolog/Func.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

-header {* Untyped functional language, with call by value semantics *}
+section {* Untyped functional language, with call by value semantics *}

theory Func
imports HOHH
--- a/src/HOL/Prolog/HOHH.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Prolog/HOHH.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

-header {* Higher-order hereditary Harrop formulas *}
+section {* Higher-order hereditary Harrop formulas *}

theory HOHH
imports HOL
--- a/src/HOL/Prolog/Test.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Prolog/Test.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

+section {* Basic examples *}

theory Test
imports HOHH
--- a/src/HOL/Prolog/Type.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Prolog/Type.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

+section {* Type inference *}

theory Type
imports Func
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

+section {* Euclid's theorem *}

theory Euclid
imports
--- a/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Helmut Schwichtenberg, LMU Muenchen
*)

-header {* Greatest common divisor *}
+section {* Greatest common divisor *}

theory Greatest_Common_Divisor
imports QuotRem
--- a/src/HOL/Proofs/Extraction/Higman.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Monika Seisenberger, LMU Muenchen
*)

+section {* Higman's lemma *}

theory Higman
imports Old_Datatype
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

-header {* The pigeonhole principle *}
+section {* The pigeonhole principle *}

theory Pigeonhole
imports Util "~~/src/HOL/Library/Code_Target_Numeral"
--- a/src/HOL/Proofs/Extraction/QuotRem.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

-header {* Quotient and remainder *}
+section {* Quotient and remainder *}

theory QuotRem
imports Util
--- a/src/HOL/Proofs/Extraction/Util.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/Util.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

-header {* Auxiliary lemmas used in program extraction examples *}
+section {* Auxiliary lemmas used in program extraction examples *}

theory Util
imports Old_Datatype
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen
*)

+section {* Warshall's algorithm *}

theory Warshall
imports Old_Datatype
--- a/src/HOL/Proofs/Lambda/Commutation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/Commutation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Abstract commutation and confluence notions *}
+section {* Abstract commutation and confluence notions *}

theory Commutation
imports Main
--- a/src/HOL/Proofs/Lambda/Eta.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Eta-reduction *}

theory Eta imports ParRed begin

--- a/src/HOL/Proofs/Lambda/InductTermi.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/InductTermi.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
rediscovered by Matthes and Joachimski.
*)

-header {* Inductive characterization of terminating lambda terms *}
+section {* Inductive characterization of terminating lambda terms *}

theory InductTermi imports ListBeta begin

--- a/src/HOL/Proofs/Lambda/Lambda.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/Lambda.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Basic definitions of Lambda-calculus *}
+section {* Basic definitions of Lambda-calculus *}

theory Lambda
imports Main
--- a/src/HOL/Proofs/Lambda/LambdaType.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Simply-typed lambda terms *}
+section {* Simply-typed lambda terms *}

theory LambdaType imports ListApplication begin

--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Application of a term to a list of terms *}
+section {* Application of a term to a list of terms *}

theory ListApplication imports Lambda begin

--- a/src/HOL/Proofs/Lambda/ListBeta.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/ListBeta.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Lifting beta-reduction to lists *}
+section {* Lifting beta-reduction to lists *}

theory ListBeta imports ListApplication ListOrder begin

--- a/src/HOL/Proofs/Lambda/ListOrder.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/ListOrder.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Lifting an order to lists of elements *}
+section {* Lifting an order to lists of elements *}

theory ListOrder
imports Main
--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer, TU Muenchen, 2003
*)

-header {* Inductive characterization of lambda terms in normal form *}
+section {* Inductive characterization of lambda terms in normal form *}

theory NormalForm
imports ListBeta
--- a/src/HOL/Proofs/Lambda/ParRed.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/ParRed.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
confluence of beta.
*)

-header {* Parallel reduction and a complete developments *}
+section {* Parallel reduction and a complete developments *}

theory ParRed imports Lambda Commutation begin

--- a/src/HOL/Proofs/Lambda/Standardization.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/Standardization.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section {* Standardization *}

theory Standardization
imports NormalForm
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Strong normalization for simply-typed lambda calculus *}
+section {* Strong normalization for simply-typed lambda calculus *}

theory StrongNorm imports LambdaType InductTermi begin

--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Weak normalization for simply-typed lambda calculus *}
+section {* Weak normalization for simply-typed lambda calculus *}

theory WeakNorm
imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
--- a/src/HOL/Proofs/ex/Hilbert_Classical.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Proofs/ex/Hilbert_Classical.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
*)

-header {* Hilbert's choice and classical logic *}
+section {* Hilbert's choice and classical logic *}

theory Hilbert_Classical
imports Main
--- a/src/HOL/Quickcheck_Examples/Completeness.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Proving completeness of exhaustive generators *}
+section {* Proving completeness of exhaustive generators *}

theory Completeness
imports Main
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Copyright   2004 - 2010 TU Muenchen
*)

-header {* Examples for the 'quickcheck' command *}
+section {* Examples for the 'quickcheck' command *}

theory Quickcheck_Examples
imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Examples for narrowing-based testing  *}
+section {* Examples for narrowing-based testing  *}

theory Quickcheck_Narrowing_Examples
imports Main
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Lukas Bulwahn, TU Muenchen *)

-header {* A simple counterexample generator performing exhaustive testing *}
+section {* A simple counterexample generator performing exhaustive testing *}

theory Quickcheck_Exhaustive
imports Quickcheck_Random
--- a/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Lukas Bulwahn, TU Muenchen *)

-header {* Counterexample generator performing narrowing-based testing *}
+section {* Counterexample generator performing narrowing-based testing *}

theory Quickcheck_Narrowing
imports Quickcheck_Random
--- a/src/HOL/Quickcheck_Random.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)

-header {* A simple counterexample generator performing random testing *}
+section {* A simple counterexample generator performing random testing *}

theory Quickcheck_Random
imports Random Code_Evaluation Enum
--- a/src/HOL/Quotient.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quotient.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Cezary Kaliszyk and Christian Urban
*)

-header {* Definition of Quotient Types *}
+section {* Definition of Quotient Types *}

theory Quotient
imports Lifting
--- a/src/HOL/Quotient_Examples/DList.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quotient_Examples/DList.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
and theory morphism version by Maksym Bortin
*)

-header {* Lists with distinct elements *}
+section {* Lists with distinct elements *}

theory DList
imports "~~/src/HOL/Library/Quotient_List"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman, TU Munich
*)

-header {* Lifting and transfer with a finite set type *}
+section {* Lifting and transfer with a finite set type *}

theory Lift_FSet
imports Main
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Ondrej Kuncar
*)

-header {* Example of lifting definitions with contravariant or co/contravariant type variables *}
+section {* Example of lifting definitions with contravariant or co/contravariant type variables *}

theory Lift_Fun
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn and Ondrej Kuncar
*)

-header {* Example of lifting definitions with the lifting infrastructure *}
+section {* Example of lifting definitions with the lifting infrastructure *}

theory Lift_Set
imports Main
--- a/src/HOL/Random.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Random.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Florian Haftmann, TU Muenchen *)

-header {* A HOL random engine *}
+section {* A HOL random engine *}

theory Random
imports List Groups_List
--- a/src/HOL/Random_Pred.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Random_Pred.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Lukas Bulwahn, TU Muenchen *)

+section {* The Random-Predicate Monad *}

theory Random_Pred
imports Quickcheck_Random
--- a/src/HOL/Random_Sequence.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Random_Sequence.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,7 +1,7 @@

(* Author: Lukas Bulwahn, TU Muenchen *)

+section {* Various kind of sequences inside the random monad *}

theory Random_Sequence
imports Random_Pred
--- a/src/HOL/Rat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Rat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel, TU Muenchen
*)

+section {* Rational numbers *}

theory Rat
imports GCD Archimedean_Field
--- a/src/HOL/Real.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Real.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Construction of Cauchy Reals by Brian Huffman, 2010
*)

-header {* Development of the Reals using Cauchy Sequences *}
+section {* Development of the Reals using Cauchy Sequences *}

theory Real
imports Rat Conditionally_Complete_Lattices
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Johannes Hölzl
*)

-header {* Vector Spaces and Algebras over the Reals *}
+section {* Vector Spaces and Algebras over the Reals *}

theory Real_Vector_Spaces
imports Real Topological_Spaces
--- a/src/HOL/Record.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Record.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Author:     Florian Haftmann, TU Muenchen
*)

-header {* Extensible records with structural subtyping *}
+section {* Extensible records with structural subtyping *}

theory Record
imports Quickcheck_Exhaustive
--- a/src/HOL/Record_Benchmark/Record_Benchmark.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Norbert Schirmer, DFKI
*)

-header {* Benchmark for large record *}
+section {* Benchmark for large record *}

theory Record_Benchmark
imports Main
--- a/src/HOL/Relation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Relation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
*)

-header {* Relations -- as sets of pairs, and binary predicates *}
+section {* Relations -- as sets of pairs, and binary predicates *}

theory Relation
imports Finite_Set
--- a/src/HOL/Rings.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Rings.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
*)

+section {* Rings *}

theory Rings
imports Groups
--- a/src/HOL/SAT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SAT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Basic setup for the 'sat' and 'satx' tactics.
*)

-header {* Reconstructing external resolution proofs for propositional logic *}
+section {* Reconstructing external resolution proofs for propositional logic *}

theory SAT
imports HOL
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Author:     Piero Tramontano
*)

+section{*The SET Cardholder Registration Protocol*}

theory Cardholder_Registration
imports Public_SET
--- a/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Lawrence C Paulson
*)

+section{*Theory of Events for SET*}

theory Event_SET
imports Message_SET
--- a/src/HOL/SET_Protocol/Merchant_Registration.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SET_Protocol/Merchant_Registration.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Lawrence C Paulson
*)

+section{*The SET Merchant Registration Protocol*}

theory Merchant_Registration
imports Public_SET
--- a/src/HOL/SET_Protocol/Message_SET.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Lawrence C Paulson
*)

-header{*The Message Theory, Modified for SET*}
+section{*The Message Theory, Modified for SET*}

theory Message_SET
imports Main "~~/src/HOL/Library/Nat_Bijection"
--- a/src/HOL/SET_Protocol/Public_SET.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Lawrence C Paulson
*)

-header{*The Public-Key Theory, Modified for SET*}
+section{*The Public-Key Theory, Modified for SET*}

theory Public_SET
imports Event_SET
--- a/src/HOL/SET_Protocol/Purchase.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Lawrence C Paulson
*)

+section{*Purchase Phase of SET*}

theory Purchase
imports Public_SET
--- a/src/HOL/SMT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SMT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Sascha Boehme, TU Muenchen
*)

-header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}
+section {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}

theory SMT
imports Divides
--- a/src/HOL/SMT_Examples/Boogie.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SMT_Examples/Boogie.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Sascha Boehme, TU Muenchen
*)

-header {* Proving Boogie-generated verification conditions *}
+section {* Proving Boogie-generated verification conditions *}

theory Boogie
imports Main
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Sascha Boehme, TU Muenchen
*)

-header {* Examples for the SMT binding *}
+section {* Examples for the SMT binding *}

theory SMT_Examples
imports Complex_Main
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Sascha Boehme, TU Muenchen
*)

-header {* Tests for the SMT binding *}
+section {* Tests for the SMT binding *}

theory SMT_Tests
imports Complex_Main
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Sascha Boehme, TU Muenchen
*)

-header {* Word examples for for SMT binding *}
+section {* Word examples for for SMT binding *}

theory SMT_Word_Examples
imports "~~/src/HOL/Word/Word"
--- a/src/HOL/Semiring_Normalization.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, TU Muenchen
*)

+section {* Semiring normalization *}

theory Semiring_Normalization
imports Numeral_Simprocs Nat_Transfer
--- a/src/HOL/Series.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Series.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
*)

+section {* Infinite Series *}

theory Series
imports Limits
--- a/src/HOL/Set.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Set.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel *)

-header {* Set theory for higher-order logic *}
+section {* Set theory for higher-order logic *}

theory Set
imports Lattices
--- a/src/HOL/Set_Interval.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -11,7 +11,7 @@
Examples: Ico = {_ ..< _} and Ici = {_ ..}
*)

+section {* Set intervals *}

theory Set_Interval
imports Lattices_Big Nat_Transfer
--- a/src/HOL/Sledgehammer.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Sledgehammer.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

+section {* Sledgehammer: Isabelle--ATP Linkup *}

theory Sledgehammer
imports Presburger SMT
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Norbert Schirmer, TU Muenchen
*)

-header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}
+section {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}

theory DistinctTreeProver
imports Main
--- a/src/HOL/Statespace/StateFun.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Statespace/StateFun.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Norbert Schirmer, TU Muenchen
*)

-header {* State Space Representation as Function \label{sec:StateFun}*}
+section {* State Space Representation as Function \label{sec:StateFun}*}

theory StateFun imports DistinctTreeProver
begin
--- a/src/HOL/Statespace/StateSpaceEx.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Norbert Schirmer, TU Muenchen
*)

+section {* Examples \label{sec:Examples} *}
theory StateSpaceEx
imports StateSpaceLocale StateSpaceSyntax
begin
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Norbert Schirmer, TU Muenchen
*)

-header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
+section {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}

theory StateSpaceLocale imports StateFun
keywords "statespace" :: thy_decl
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Norbert Schirmer, TU Muenchen
*)

-header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
+section {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
theory StateSpaceSyntax
imports StateSpaceLocale
begin
--- a/src/HOL/String.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/String.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)

-header {* Character and string types *}
+section {* Character and string types *}

theory String
imports Enum
--- a/src/HOL/Sum_Type.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*The Disjoint Sum of Two Types*}
+section{*The Disjoint Sum of Two Types*}

theory Sum_Type
imports Typedef Inductive Fun
--- a/src/HOL/TLA/Action.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Action.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The action level of TLA as an Isabelle theory *}
+section {* The action level of TLA as an Isabelle theory *}

theory Action
imports Stfun
--- a/src/HOL/TLA/Buffer/Buffer.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* A simple FIFO buffer (synchronous communication, interleaving) *}
+section {* A simple FIFO buffer (synchronous communication, interleaving) *}

theory Buffer
imports TLA
--- a/src/HOL/TLA/Buffer/DBuffer.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Buffer/DBuffer.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* Two FIFO buffers in a row, with interleaving assumption *}
+section {* Two FIFO buffers in a row, with interleaving assumption *}

theory DBuffer
imports Buffer
--- a/src/HOL/TLA/Inc/Inc.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Inc/Inc.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* Lamport's "increment" example *}
+section {* Lamport's "increment" example *}

theory Inc
imports TLA
--- a/src/HOL/TLA/Intensional.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* A framework for "intensional" (possible-world based) logics
+section {* A framework for "intensional" (possible-world based) logics
on top of HOL, with lifting of constants and functions *}

theory Intensional
--- a/src/HOL/TLA/Memory/MemClerk.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: specification of the memory clerk *}
+section {* RPC-Memory example: specification of the memory clerk *}

theory MemClerk
imports Memory RPC MemClerkParameters
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: Parameters of the memory clerk *}
+section {* RPC-Memory example: Parameters of the memory clerk *}

theory MemClerkParameters
imports RPCParameters
--- a/src/HOL/TLA/Memory/Memory.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: Memory specification *}
+section {* RPC-Memory example: Memory specification *}

theory Memory
imports MemoryParameters ProcedureInterface
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: Memory implementation *}
+section {* RPC-Memory example: Memory implementation *}

theory MemoryImplementation
imports Memory RPC MemClerk
--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: Memory parameters *}
+section {* RPC-Memory example: Memory parameters *}

theory MemoryParameters
imports RPCMemoryParams
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* Procedure interface for RPC-Memory components *}
+section {* Procedure interface for RPC-Memory components *}

theory ProcedureInterface
imports "../TLA" RPCMemoryParams
--- a/src/HOL/TLA/Memory/RPC.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: RPC specification *}
+section {* RPC-Memory example: RPC specification *}

theory RPC
imports RPCParameters ProcedureInterface Memory
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* Basic declarations for the RPC-memory example *}
+section {* Basic declarations for the RPC-memory example *}

theory RPCMemoryParams
imports Main
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Stephan Merz, University of Munich
*)

-header {* RPC-Memory example: RPC parameters *}
+section {* RPC-Memory example: RPC parameters *}

theory RPCParameters
imports MemoryParameters
--- a/src/HOL/TLA/Stfun.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/Stfun.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* States and state functions for TLA as an "intensional" logic *}
+section {* States and state functions for TLA as an "intensional" logic *}

theory Stfun
imports Intensional
--- a/src/HOL/TLA/TLA.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TLA/TLA.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* The temporal level of TLA *}
+section {* The temporal level of TLA *}

theory TLA
imports Init
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

-header {* ATP Problem Importer *}
+section {* ATP Problem Importer *}

theory ATP_Problem_Import
imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

-header {* ATP Theory Exporter *}
+section {* ATP Theory Exporter *}

theory ATP_Theory_Export
imports Complex_Main
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

-header {* MaSh Evaluation Driver *}
+section {* MaSh Evaluation Driver *}

theory MaSh_Eval
imports MaSh_Export_Base
--- a/src/HOL/TPTP/MaSh_Export.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

+section {* MaSh Exporter *}

theory MaSh_Export
imports MaSh_Export_Base
--- a/src/HOL/TPTP/MaSh_Export_Base.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Jasmin Blanchette, TU Muenchen
*)

-header {* MaSh Exporter Base *}
+section {* MaSh Exporter Base *}

theory MaSh_Export_Base
imports Main
--- a/src/HOL/Taylor.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Taylor.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
*)

+section {* Taylor series *}

theory Taylor
imports MacLaurin
--- a/src/HOL/Topological_Spaces.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Johannes Hölzl
*)

+section {* Topological Spaces *}

theory Topological_Spaces
imports Main Conditionally_Complete_Lattices
--- a/src/HOL/Transcendental.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Transcendental.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
*)

+section{*Power Series, Transcendental Functions etc.*}

theory Transcendental
imports Fact Series Deriv NthRoot
--- a/src/HOL/Transfer.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Transfer.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Ondrej Kuncar, TU Muenchen
*)

-header {* Generic theorem transfer using relations *}
+section {* Generic theorem transfer using relations *}

theory Transfer
imports Hilbert_Choice Metis Option
--- a/src/HOL/Transitive_Closure.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Reflexive and Transitive closure of a relation *}
+section {* Reflexive and Transitive closure of a relation *}

theory Transitive_Closure
imports Relation
--- a/src/HOL/Typedef.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Typedef.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Munich
*)

-header {* HOL type definitions *}
+section {* HOL type definitions *}

theory Typedef
imports Set
--- a/src/HOL/Typerep.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Typerep.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)

-header {* Reflecting Pure types into HOL *}
+section {* Reflecting Pure types into HOL *}

theory Typerep
imports String
--- a/src/HOL/UNITY/Comp.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
Technical Report 2000-003, University of Florida, 2000.
*)

+section{*Composition: Basic Primitives*}

theory Comp
imports Union
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Common Declarations for Chandy and Charpentier's Allocator*}
+section{*Common Declarations for Chandy and Charpentier's Allocator*}

theory AllocBase imports "../UNITY_Main" begin

--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Implementation of a multiple-client allocator from a single-client allocator*}
+section{*Implementation of a multiple-client allocator from a single-client allocator*}

theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin

--- a/src/HOL/UNITY/Comp/Client.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/Client.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*Distributed Resource Management System: the Client*}
+section{*Distributed Resource Management System: the Client*}

theory Client imports "../Rename" AllocBase begin

--- a/src/HOL/UNITY/Comp/Counter.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/Counter.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
Springer LNCS 1586 (1999), pages 1215-1227.
*)

-header{*A Family of Similar Counters: Original Version*}
+section{*A Family of Similar Counters: Original Version*}

theory Counter imports "../UNITY_Main" begin

--- a/src/HOL/UNITY/Comp/Counterc.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -11,7 +11,7 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)

-header{*A Family of Similar Counters: Version with Compatibility*}
+section{*A Family of Similar Counters: Version with Compatibility*}

theory Counterc imports "../UNITY_Main" begin

--- a/src/HOL/UNITY/Comp/Priority.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*The priority system*}

theory Priority imports PriorityAux begin

--- a/src/HOL/UNITY/Comp/Progress.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
David Meier's thesis
*)

+section{*Progress Set Examples*}

theory Progress imports "../UNITY_Main" begin

--- a/src/HOL/UNITY/Constrains.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Constrains.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Weak safety relations: restricted to the set of reachable states.
*)

+section{*Weak Safety*}

theory Constrains imports UNITY begin

--- a/src/HOL/UNITY/Detects.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Detects.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)

+section{*The Detects Relation*}

theory Detects imports FP SubstAx begin

--- a/src/HOL/UNITY/ELT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/ELT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -21,7 +21,7 @@
monos Pow_mono
*)

+section{*Progress Under Allowable Sets*}

theory ELT imports Project begin

--- a/src/HOL/UNITY/Extend.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Extend.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
function g (forgotten) maps the extended state to the "extending part"
*)

+section{*Extending State Sets*}

theory Extend imports Guar begin

--- a/src/HOL/UNITY/FP.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/FP.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)

+section{*Fixed Point of a Program*}

theory FP imports UNITY begin

--- a/src/HOL/UNITY/Follows.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Follows.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header{*The Follows Relation of Charpentier and Sivilotte*}
+section{*The Follows Relation of Charpentier and Sivilotte*}

theory Follows
imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
--- a/src/HOL/UNITY/Guar.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Guar.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -10,7 +10,7 @@
Fifth International Conference on Mathematics of Program, 2000.
*)

+section{*Guarantees Specifications*}

theory Guar
imports Comp
--- a/src/HOL/UNITY/Lift_prog.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
lift_prog, etc: replication of components and arrays of processes.
*)

+section{*Replication of Components*}

theory Lift_prog imports Rename begin

--- a/src/HOL/UNITY/ListOrder.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -10,7 +10,7 @@
Also overloads <= and < for lists!
*)

-header {*The Prefix Ordering on Lists*}
+section {*The Prefix Ordering on Lists*}

theory ListOrder
imports Main
--- a/src/HOL/UNITY/ProgressSets.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -13,7 +13,7 @@
Swiss Federal Institute of Technology Zurich (1997)
*)

+section{*Progress Sets*}

theory ProgressSets imports Transformers begin

--- a/src/HOL/UNITY/Project.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Project.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
Inheritance of GUARANTEES properties under extension.
*)

+section{*Projections of State Sets*}

theory Project imports Extend begin

--- a/src/HOL/UNITY/Rename.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Rename.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Renaming of State Sets*}

theory Rename imports Extend begin

--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
*)

-header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
+section{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}

theory NSP_Bad imports "../../Auth/Public" "../UNITY_Main" begin

--- a/src/HOL/UNITY/Simple/Token.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
*)

+section {*The Token Ring*}

theory Token
imports "../WFair"
--- a/src/HOL/UNITY/SubstAx.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Weak LeadsTo relation (restricted to the set of reachable states)
*)

+section{*Weak Progress*}

theory SubstAx imports WFair Constrains begin

--- a/src/HOL/UNITY/Transformers.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -13,7 +13,7 @@
Swiss Federal Institute of Technology Zurich (1997)
*)

+section{*Predicate Transformers*}

theory Transformers imports Comp begin

--- a/src/HOL/UNITY/UNITY.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994.
*)

+section {*The Basic UNITY Theory*}

theory UNITY imports Main begin

--- a/src/HOL/UNITY/UNITY_Main.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Comprehensive UNITY Theory*}

theory UNITY_Main
imports Detects PPROD Follows ProgressSets
--- a/src/HOL/UNITY/Union.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/Union.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs.
*)

+section{*Unions of Programs*}

theory Union imports SubstAx FP begin

--- a/src/HOL/UNITY/WFair.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/UNITY/WFair.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)

+section{*Progress*}

theory WFair imports UNITY begin

--- a/src/HOL/Unix/Nested_Environment.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Unix/Nested_Environment.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Muenchen
*)

+section \<open>Nested environments\<close>

theory Nested_Environment
imports Main
--- a/src/HOL/Unix/Unix.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Unix/Unix.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Muenchen
*)

+section \<open>Unix file-systems \label{sec:unix-file-system}\<close>

theory Unix
imports
--- a/src/HOL/Wellfounded.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Author:     Andrei Popescu, TU Muenchen
*)

+section {*Well-founded Recursion*}

theory Wellfounded
imports Transitive_Closure
--- a/src/HOL/Wfrec.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Wfrec.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
*)

-header {* Well-Founded Recursion Combinator *}
+section {* Well-Founded Recursion Combinator *}

theory Wfrec
imports Wellfounded
--- a/src/HOL/Zorn.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/Zorn.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -7,7 +7,7 @@
The well-ordering theorem.
*)

+section {* Zorn's Lemma *}

theory Zorn
imports Order_Relation Hilbert_Choice
--- a/src/HOL/ex/Abstract_NAT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Makarius
*)

-header {* Abstract Natural Numbers primitive recursion *}
+section {* Abstract Natural Numbers primitive recursion *}

theory Abstract_NAT
imports Main
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
@@ -2,7 +2,7 @@
Author:     Christian Sternagel
*)

imports
--- a/src/HOL/ex/Antiquote.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Antiquote.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Muenchen
*)

+section {* Antiquotations *}

theory Antiquote
imports Main
--- a/src/HOL/ex/Arith_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Tjark Weber
*)

+section {* Arithmetic *}

theory Arith_Examples
imports Main
--- a/src/HOL/ex/BT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/BT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Binary trees
*)

+section {* Binary trees *}

theory BT imports Main begin

--- a/src/HOL/ex/BinEx.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/BinEx.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Binary arithmetic examples *}
+section {* Binary arithmetic examples *}

theory BinEx
imports Complex_Main
--- a/src/HOL/ex/Birthday_Paradox.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Birthday_Paradox.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn, TU Muenchen, 2007
*)

+section {* A Formulation of the Birthday Paradox *}

imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
--- a/src/HOL/ex/Bubblesort.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Bubblesort.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)

+section {* Bubblesort *}

theory Bubblesort
imports "~~/src/HOL/Library/Multiset"
--- a/src/HOL/ex/CTL.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/CTL.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer
*)

+section {* CTL formulae *}

theory CTL
imports Main
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* Some examples with text cartouches *}
+section {* Some examples with text cartouches *}

theory Cartouche_Examples
imports Main
--- a/src/HOL/ex/Case_Product.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Case_Product.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Examples for the 'case_product' attribute *}
+section {* Examples for the 'case_product' attribute *}

theory Case_Product
imports Main
--- a/src/HOL/ex/Chinese.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Chinese.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
formal and informal ones.
*)

-header {* A Chinese theory *}
+section {* A Chinese theory *}

theory Chinese imports Main begin

--- a/src/HOL/ex/Classical.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Classical.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Classical Predicate Calculus Problems*}

theory Classical imports Main begin

--- a/src/HOL/ex/Code_Binary_Nat_examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Code_Binary_Nat_examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Florian Haftmann, TU Muenchen
*)

-header {* Simple examples for natural numbers implemented in binary representation. *}
+section {* Simple examples for natural numbers implemented in binary representation. *}

theory Code_Binary_Nat_examples
imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat"
--- a/src/HOL/ex/Coherent.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Coherent.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
*)

-header {* Coherent Logic Problems *}
+section {* Coherent Logic Problems *}

theory Coherent
imports Main
--- a/src/HOL/ex/Eval_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Eval_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)

-header {* Small examples for evaluation mechanisms *}
+section {* Small examples for evaluation mechanisms *}

theory Eval_Examples
imports Complex_Main
--- a/src/HOL/ex/Execute_Choice.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Execute_Choice.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)

-header {* A simple cookbook example how to eliminate choice in programs. *}
+section {* A simple cookbook example how to eliminate choice in programs. *}

theory Execute_Choice
imports Main "~~/src/HOL/Library/AList_Mapping"
--- a/src/HOL/ex/FinFunPred.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/FinFunPred.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Author:     Andreas Lochbihler *)

+section {*
Predicates modelled as FinFuns
*}

--- a/src/HOL/ex/Fundefs.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Fundefs.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Alexander Krauss, TU Muenchen
*)

-header {* Examples of function definitions *}
+section {* Examples of function definitions *}

theory Fundefs
imports Main "~~/src/HOL/Library/Monad_Syntax"
--- a/src/HOL/ex/Gauge_Integration.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy .
*)

-header{*Theory of Integration on real intervals*}
+section{*Theory of Integration on real intervals*}

theory Gauge_Integration
imports Complex_Main
--- a/src/HOL/ex/Groebner_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Groebner_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, TU Muenchen
*)

-header {* Groebner Basis Examples *}
+section {* Groebner Basis Examples *}

theory Groebner_Examples
imports Groebner_Basis
--- a/src/HOL/ex/Guess.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Guess.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Makarius
*)

-header {* Proof by guessing *}
+section {* Proof by guessing *}

theory Guess
imports Main
--- a/src/HOL/ex/HarmonicSeries.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Benjamin Porter, 2006
*)

-header {* Divergence of the Harmonic Series *}
+section {* Divergence of the Harmonic Series *}

theory HarmonicSeries
imports Complex_Main
--- a/src/HOL/ex/Hebrew.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Hebrew.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
formal and informal ones.
*)

-header {* A Hebrew theory *}
+section {* A Hebrew theory *}

theory Hebrew
imports Main
--- a/src/HOL/ex/Hex_Bin_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Hex_Bin_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gerwin Klein, NICTA
*)

+section {* Examples for hexadecimal and binary numerals *}

theory Hex_Bin_Examples imports Main
begin
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
*)

-header {* Foundations of HOL *}
+section {* Foundations of HOL *}

theory Higher_Order_Logic imports Pure begin

--- a/src/HOL/ex/Iff_Oracle.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Iff_Oracle.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:     Makarius
*)

-header {* Example of Declaring an Oracle *}
+section {* Example of Declaring an Oracle *}

theory Iff_Oracle
imports Main
--- a/src/HOL/ex/Induction_Schema.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Induction_Schema.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Alexander Krauss, TU Muenchen
*)

-header {* Examples of automatically derived induction rules *}
+section {* Examples of automatically derived induction rules *}

theory Induction_Schema
imports Main
--- a/src/HOL/ex/Intuitionistic.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Intuitionistic.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Taken from FOL/ex/int.ML
*)

-header {* Higher-Order Logic: Intuitionistic predicate calculus problems *}
+section {* Higher-Order Logic: Intuitionistic predicate calculus problems *}

theory Intuitionistic imports Main begin

--- a/src/HOL/ex/Lagrange.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Lagrange.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* A lemma for Lagrange's theorem *}
+section {* A lemma for Lagrange's theorem *}

theory Lagrange imports Main begin

--- a/src/HOL/ex/List_to_Set_Comprehension_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/List_to_Set_Comprehension_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Examples for the list comprehension to set comprehension simproc *}
+section {* Examples for the list comprehension to set comprehension simproc *}

theory List_to_Set_Comprehension_Examples
imports Main
--- a/src/HOL/ex/LocaleTest2.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -8,7 +8,7 @@
which is FOL/ex/LocaleTest.thy
*)

-header {* Test of Locale Interpretation *}
+section {* Test of Locale Interpretation *}

theory LocaleTest2
imports Main GCD
--- a/src/HOL/ex/ML.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/ML.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Makarius
*)

+section \<open>Isabelle/ML basics\<close>

theory "ML"
imports Main
--- a/src/HOL/ex/MT.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/MT.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -12,7 +12,7 @@
Report 308, Computer Lab, University of Cambridge (1993).
*)

-header {* Milner-Tofte: Co-induction in Relational Semantics *}
+section {* Milner-Tofte: Co-induction in Relational Semantics *}

theory MT
imports Main
--- a/src/HOL/ex/MergeSort.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/MergeSort.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

+section{*Merge Sort*}

theory MergeSort
imports "~~/src/HOL/Library/Multiset"
--- a/src/HOL/ex/Meson_Test.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Meson_Test.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,5 +1,5 @@

-header {* Meson test cases *}
+section {* Meson test cases *}

theory Meson_Test
imports Main
--- a/src/HOL/ex/MonoidGroup.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/MonoidGroup.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel
*)

-header {* Monoids and Groups as predicates over record schemes *}
+section {* Monoids and Groups as predicates over record schemes *}

theory MonoidGroup imports Main begin

--- a/src/HOL/ex/Multiquote.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Multiquote.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, TU Muenchen
*)

-header {* Multiple nested quotations and anti-quotations *}
+section {* Multiple nested quotations and anti-quotations *}

theory Multiquote
imports Main
--- a/src/HOL/ex/NatSum.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/NatSum.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow
*)

-header {* Summing natural numbers *}
+section {* Summing natural numbers *}

theory NatSum imports Main begin

--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(*  Authors:  Klaus Aehlig, Tobias Nipkow *)

-header {* Testing implementation of normalization by evaluation *}
+section {* Testing implementation of normalization by evaluation *}

theory Normalization_by_Evaluation
imports Complex_Main
--- a/src/HOL/ex/PER.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/PER.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen
*)

-header {* Partial equivalence relations *}
+section {* Partial equivalence relations *}

theory PER imports Main begin

--- a/src/HOL/ex/Parallel_Example.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Parallel_Example.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
+section {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}

theory Parallel_Example
imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
--- a/src/HOL/ex/PresburgerEx.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/PresburgerEx.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, TU Muenchen
*)

-header {* Some examples for Presburger Arithmetic *}
+section {* Some examples for Presburger Arithmetic *}

theory PresburgerEx
imports Presburger
--- a/src/HOL/ex/Primrec.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Primrec.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
Primitive Recursive Functions.
*)

-header {* Primitive Recursive Functions *}
+section {* Primitive Recursive Functions *}

theory Primrec imports Main begin

--- a/src/HOL/ex/Quicksort.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Quicksort.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
*)

-header {* Quicksort with function package *}
+section {* Quicksort with function package *}

theory Quicksort
imports "~~/src/HOL/Library/Multiset"
--- a/src/HOL/ex/Records.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Records.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
TU Muenchen
*)

-header {* Using extensible records in HOL -- points and coloured points *}
+section {* Using extensible records in HOL -- points and coloured points *}

theory Records
imports Main
--- a/src/HOL/ex/Reflection_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Reflection_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, TU Muenchen
*)

-header {* Examples for generic reflection and reification *}
+section {* Examples for generic reflection and reification *}

theory Reflection_Examples
imports Complex_Main "~~/src/HOL/Library/Reflection"
--- a/src/HOL/ex/Refute_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
See HOL/Refute.thy for help.
*)

-header {* Examples for the 'refute' command *}
+section {* Examples for the 'refute' command *}

theory Refute_Examples
imports "~~/src/HOL/Library/Refute"
--- a/src/HOL/ex/SAT_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Examples for proof methods "sat" and "satx" *}
+section {* Examples for proof methods "sat" and "satx" *}

theory SAT_Examples
imports Main
--- a/src/HOL/ex/SVC_Oracle.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -5,7 +5,7 @@
Based upon the work of Søren T. Heilmann.
*)

-header {* Installing an oracle for SVC (Stanford Validity Checker) *}
+section {* Installing an oracle for SVC (Stanford Validity Checker) *}

theory SVC_Oracle
imports Main
--- a/src/HOL/ex/Seq.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Seq.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Makarius
*)

+section \<open>Finite sequences\<close>

theory Seq
imports Main
--- a/src/HOL/ex/Serbian.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Serbian.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Conversion between Serbian cyrillic and latin letters (српска ћирилица и латиница)
*)

-header {* A Serbian theory *}
+section {* A Serbian theory *}

theory Serbian
imports Main
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Examples for the set comprehension to pointfree simproc *}
+section {* Examples for the set comprehension to pointfree simproc *}

theory Set_Comprehension_Pointfree_Examples
imports Main
--- a/src/HOL/ex/Set_Theory.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Set_Theory.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
+section {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}

theory Set_Theory
imports Main
--- a/src/HOL/ex/Simproc_Tests.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman
*)

-header {* Testing of arithmetic simprocs *}
+section {* Testing of arithmetic simprocs *}

theory Simproc_Tests
imports Main
--- a/src/HOL/ex/Sqrt.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Sqrt.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Markus Wenzel, Tobias Nipkow, TU Muenchen
*)

-header {*  Square roots of primes are irrational *}
+section {*  Square roots of primes are irrational *}

theory Sqrt
imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
--- a/src/HOL/ex/Sqrt_Script.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Sqrt_Script.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Square roots of primes are irrational (script version) *}
+section {* Square roots of primes are irrational (script version) *}

theory Sqrt_Script
imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
--- a/src/HOL/ex/Sudoku.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Sudoku.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* A SAT-based Sudoku Solver *}
+section {* A SAT-based Sudoku Solver *}

theory Sudoku
imports Main
--- a/src/HOL/ex/Tarski.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Tarski.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Florian Kammüller, Cambridge University Computer Laboratory
*)

-header {* The Full Theorem of Tarski *}
+section {* The Full Theorem of Tarski *}

theory Tarski
imports Main "~~/src/HOL/Library/FuncSet"
--- a/src/HOL/ex/Termination.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Termination.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
Author:      Alexander Krauss, TU Muenchen
*)

-header {* Examples and regression tests for automated termination proofs *}
+section {* Examples and regression tests for automated termination proofs *}

theory Termination
imports Main "~~/src/HOL/Library/Multiset"
--- a/src/HOL/ex/ThreeDivides.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Benjamin Porter, 2005
*)

-header {* Three Divides Theorem *}
+section {* Three Divides Theorem *}

theory ThreeDivides
imports Main "~~/src/HOL/Library/LaTeXsugar"
--- a/src/HOL/ex/Transfer_Ex.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Transfer_Ex.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,5 +1,5 @@

-header {* Various examples for transfer procedure *}
+section {* Various examples for transfer procedure *}

theory Transfer_Ex
imports Main Transfer_Int_Nat
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Brian Huffman, TU Muenchen
*)

-header {* Using the transfer method between nat and int *}
+section {* Using the transfer method between nat and int *}

theory Transfer_Int_Nat
imports GCD
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)

-header {* Simple example for table-based implementation of the reflexive transitive closure *}
+section {* Simple example for table-based implementation of the reflexive transitive closure *}

theory Transitive_Closure_Table_Ex
imports "~~/src/HOL/Library/Transitive_Closure_Table"
--- a/src/HOL/ex/Tree23.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Tree23.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Tobias Nipkow, TU Muenchen
*)

+section {* 2-3 Trees *}

theory Tree23
imports Main
--- a/src/HOL/ex/Unification.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/Unification.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -4,7 +4,7 @@
Author:     Alexander Krauss, TUM
*)

-header {* Substitution and Unification *}
+section {* Substitution and Unification *}

theory Unification
imports Main
--- a/src/HOL/ex/While_Combinator_Example.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/While_Combinator_Example.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* An application of the While combinator *}
+section {* An application of the While combinator *}

theory While_Combinator_Example
imports "~~/src/HOL/Library/While_Combinator"
--- a/src/HOL/ex/svc_test.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/HOL/ex/svc_test.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
-header {* Demonstrating the interface SVC *}
+section {* Demonstrating the interface SVC *}

theory svc_test
imports SVC_Oracle
--- a/src/LCF/LCF.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/LCF/LCF.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* LCF on top of First-Order Logic *}
+section {* LCF on top of First-Order Logic *}

theory LCF
imports "~~/src/FOL/FOL"
--- a/src/LCF/ex/Ex1.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/LCF/ex/Ex1.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section {*  Section 10.4 *}

theory Ex1
imports LCF
--- a/src/LCF/ex/Ex2.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/LCF/ex/Ex2.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section {* Example 3.8 *}

theory Ex2
imports LCF
--- a/src/LCF/ex/Ex3.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/LCF/ex/Ex3.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,4 +1,4 @@
+section {* Addition with fixpoint of successor *}

theory Ex3
imports LCF
--- a/src/LCF/ex/Ex4.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/LCF/ex/Ex4.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -1,5 +1,5 @@

+section {* Prefixpoints *}

theory Ex4
imports LCF
--- a/src/Sequents/LK/Nat.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Sequents/LK/Nat.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+section {* Theory of the natural numbers: Peano's axioms, primitive recursion *}

theory Nat
imports "../LK"
--- a/src/Sequents/LK/Propositional.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Sequents/LK/Propositional.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Classical sequent calculus: examples with propositional connectives *}
+section {* Classical sequent calculus: examples with propositional connectives *}

theory Propositional
imports "../LK"
--- a/src/Sequents/LK0.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Sequents/LK0.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -6,7 +6,7 @@
(eta-expanded, beta-contracted).
*)

-header {* Classical First-Order Sequent Calculus *}
+section {* Classical First-Order Sequent Calculus *}

theory LK0
imports Sequents
--- a/src/Sequents/Sequents.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Sequents/Sequents.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -3,7 +3,7 @@
*)

-header {* Parsing and pretty-printing of sequences *}
+section {* Parsing and pretty-printing of sequences *}

theory Sequents
imports Pure
--- a/src/Tools/Adhoc_Overloading.thy	Sun Nov 02 18:21:14 2014 +0100
@@ -2,7 +2,7 @@
Author: Christian Sternagel, University of Innsbruck
*)

imports Pure
--- a/src/Tools/Code_Generator.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Tools/Code_Generator.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:  Florian Haftmann, TU Muenchen
*)

theory Code_Generator
imports Pure
--- a/src/Tools/Permanent_Interpretation.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Tools/Permanent_Interpretation.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:  Florian Haftmann, TU Muenchen
*)

-header {* Permanent interpretation accompanied with mixin definitions. *}
+section {* Permanent interpretation accompanied with mixin definitions. *}

theory Permanent_Interpretation
imports Pure
--- a/src/Tools/SML/Examples.thy	Sun Nov 02 18:21:14 2014 +0100
+++ b/src/Tools/SML/Examples.thy	Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author:     Makarius
*)

-header \<open>Standard ML within the Isabelle environment\<close>
+section \<open>Standard ML within the Isabelle environment\<close>

theory Examples
imports Pure`