--- 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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-header {* Elementary arithmetic *}
+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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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).
*)
-header "Examples with elimination rules"
+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 @@
Copyright 1991 University of Cambridge
*)
-header "Equality reasoning by rewriting"
+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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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
*)
-header \<open>Barendregt's Lambda-Cube\<close>
+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 @@
-header \<open>Lambda Cube Examples\<close>
+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 @@
-header \<open>Example: First-Order Logic\<close>
+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 @@
-header{*Examples of Classical Reasoning*}
+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 @@
-header{*Examples of Intuitionistic Reasoning*}
+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 @@
-header {* Records \label{sec:records} *}
+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 @@
Copyright 1994 University of Cambridge
*)
-header{*Classical Predicate Calculus Problems*}
+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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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
*)
-header {* Natural numbers *}
+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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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
*)
-header{*The Certified Electronic Mail Protocol by Abadi et al.*}
+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 @@
Copyright 2001 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
Copyright 2001 University of Cambridge
*)
-header {*Extensions to Standard Theories*}
+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 @@
Copyright 2002 University of Cambridge
*)
-header{*Protocol-Independent Confidentiality Theorem on Nonces*}
+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
*)
-header{*protocol-independent confidentiality theorem on keys*}
+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).
*)
-header{*Needham-Schroeder-Lowe Public-Key Protocol*}
+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 @@
Copyright 2002 University of Cambridge
*)
-header{*Otway-Rees Protocol*}
+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 @@
Copyright 2002 University of Cambridge
*)
-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 @@
Copyright 2002 University of Cambridge
*)
-header{*Yahalom Protocol*}
+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 @@
Copyright 2001 University of Cambridge
*)
-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.
*)
-header{*Protocol P1*}
+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.
*)
-header{*Protocol P2*}
+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 @@
Copyright 2002 University of Cambridge
*)
-header{*Other Protocol-Independent Results*}
+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 @@
Copyright 1998 University of Cambridge
*)
-header{*The Kerberos Protocol, Version IV*}
+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 @@
Copyright 1998 University of Cambridge
*)
-header{*The Kerberos Protocol, Version IV*}
+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
*)
-header{*The Kerberos Protocol, Version V*}
+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 @@
Copyright 1998 University of Cambridge
*)
-header{*The Kerberos Protocol, BAN Version*}
+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).
*)
-header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*}
+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)
*)
-header{*Verifying the Needham-Schroeder Public-Key Protocol*}
+section{*Verifying the Needham-Schroeder Public-Key Protocol*}
theory NS_Public_Bad imports Public begin
--- 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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Original Otway-Rees Protocol*}
+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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Otway-Rees Protocol as Modified by Abadi and Needham*}
+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*}
theory OtwayRees_Bad imports Public begin
--- 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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Otway-Bull Recursive Authentication Protocol*}
+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 @@
Copyright 1996 University of Cambridge
*)
-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
*)
-header{*Original Shoup-Rubin protocol*}
+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
*)
-header{*Theory of smartcards*}
+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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Woo-Lam Protocol*}
+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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Yahalom Protocol*}
+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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Yahalom Protocol, Variant 2*}
+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 @@
Copyright 1996 University of Cambridge
*)
-header{*The Yahalom Protocol: A Flawed Version*}
+section{*The Yahalom Protocol: A Flawed Version*}
theory Yahalom_Bad imports Public begin
--- 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.
*)
-header {* 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.
*)
-header {* 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
*)
-header {* Order Union *}
+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.
*)
-header {* 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.
*)
-header {* 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.
*)
-header {* 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.
*)
-header {* Coinduction Method *}
+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 *)
-header {* Complete lattices *}
+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
*)
-header {* Conditionally-complete Lattices *}
+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.
*)
-header {* 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.
*)
-header {* 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.
*)
-header {* 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.
*)
-header {* 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.
*)
-header {* 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
*)
-header{* Differentiation *}
+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 @@
Copyright 1999 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
The integer version of factorial and other additions by Jeremy Avigad.
*)
-header{*Factorial Function*}
+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 @@
Author: Jeremy Avigad
*)
-header {* Fields *}
+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
*)
-header {* Finite sets *}
+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 @@
Copyright 1994, 2012
*)
-header {* Notions about functions *}
+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
*)
-header {* Groebner bases *}
+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 @@
with contributions by Jeremy Avigad
*)
-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
*)
-header \<open>Bounds\<close>
+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
*)
-header \<open>An order on functions\<close>
+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
*)
-header \<open>The Hahn-Banach Theorem\<close>
+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
*)
-header \<open>Extending non-maximal functions\<close>
+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
*)
-header \<open>Linearforms\<close>
+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
*)
-header \<open>Normed vector spaces\<close>
+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
*)
-header \<open>Subspaces\<close>
+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
*)
-header \<open>Vector spaces\<close>
+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
*)
-header \<open>Zorn's Lemma\<close>
+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 @@
Copyright 2001 University of Cambridge
*)
-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 @@
-header "Arithmetic and Boolean Expressions"
+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 @@
-header "Stack Machine and Compilation"
+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 *)
-header "Denotational Abstract Interpretation"
+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 *)
-header "Abstract Interpretation (ITP)"
+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 *)
-header "Compiler for IMP"
+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 @@
-header "Abstract Interpretation"
+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 *)
-header "Denotational Semantics of Commands"
+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 *)
-header "Hoare Logic"
+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 *)
-header "Live Variable Analysis"
+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 @@
-header "Security Type Systems"
+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 @@
-header "Constant Folding"
+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 @@
-header "Small-Step Semantics of Commands"
+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 @@
-header "A Typed Language"
+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 *)
-header "Definite Initialization Analysis"
+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 @@
Copyright 1999 TUM
*)
-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 @@
Copyright 1994 TU Muenchen
*)
-header {* Action signatures *}
+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 @@
Copyright 1994 TU Muenchen
*)
-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 @@
Copyright 1994 TU Muenchen
*)
-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
*)
-header {* Monadic arrays *}
+section {* Monadic arrays *}
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 *}
theory Heap_Monad
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
*)
-header {* Entry point into monadic imperative HOL *}
+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
*)
-header {* Monadic imperative HOL with examples *}
+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
*)
-header {* Monadic references *}
+section {* Monadic references *}
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
*)
-header {* Linked Lists by ML references *}
+section {* Linked Lists by ML references *}
theory Linked_Lists
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
*)
-header {* Theorems about sub arrays *}
+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 @@
Copyright 1996 University of Cambridge
*)
-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
*)
-header {* Ordinals *}
+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 @@
Copyright 2004 University of Cambridge
*)
-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 @@
Copyright 2004 University of Cambridge
*)
-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
*)
-header {* Sigma algebras *}
+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
*)
-header {* Abstract lattices *}
+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 @@
with contributions by Jeremy Avigad
*)
-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 *)
-header {* Lazy sequences *}
+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
*)
-header {* Lifting package *}
+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 @@
Author: Jeremy Avigad
*)
-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
*)
-header{*MacLaurin Series*}
+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 @@
-header {* Main HOL *}
+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.
*)
-header {* Maps *}
+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 @@
Copyright 2001 University of Cambridge
*)
-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.
*)
-header {*
+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.
*)
-header {*
+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
*)
-header "Axiomatic Semantics"
+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 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-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 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-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 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-header "Example"
+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 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-header "Operational Evaluation Semantics"
+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 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-header "Program State"
+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
*)
-header "Statements and expression emulations"
+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
*)
-header "Type relations"
+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).
*)
-header {* Natural numbers *}
+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 @@
Refute examples adapted to Nitpick.
*)
-header {* Refute Examples Adapted to Nitpick *}
+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.
*)
-header {* 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 @@
Copyright 2005, 2008 TU Muenchen
*)
-header {* Standardization *}
+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
*)
-header {* Binary Numerals *}
+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.
*)
-header {* Binomial *}
+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.
*)
-header {* Congruence *}
+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 @@
Jeremy Avigad.
*)
-header {* Fib *}
+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
*)
-header {* Gauss' Lemma *}
+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 @@
*)
-header {* Primes *}
+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.
*)
-header {* Residue rings *}
+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.
*)
-header {* UniqueFactorization *}
+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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-header {* Euler's criterion *}
+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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Copyright 1997 University of Cambridge
*)
-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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-header {* Gauss' Lemma *}
+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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-header {*Integers: Divisibility and Congruences*}
+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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
Copyright 1996 University of Cambridge
*)
-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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-header {* The law of Quadratic reciprocity *}
+section {* The law of Quadratic reciprocity *}
theory 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 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-header {* Residue Sets *}
+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 @@
Copyright 2000 University of Cambridge
*)
-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 @@
Copyright 2000 University of Cambridge
*)
-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
*)
-header {* Datatype option *}
+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
*)
-header {* Abstract orderings *}
+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 @@
Copyright 1997 University of Cambridge
*)
-header {* Exponentiation *}
+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 @@
Copyright 1992 University of Cambridge
*)
-header {* Cartesian products *}
+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)
*)
-header {* Basic examples *}
+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)
*)
-header {* Type inference *}
+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
*)
-header {* Euclid's theorem *}
+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
*)
-header {* Higman's lemma *}
+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
*)
-header {* Warshall's algorithm *}
+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 @@
Copyright 1995 TU Muenchen
*)
-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 @@
Copyright 1995, 2005 TU Muenchen
*)
-header {* Eta-reduction *}
+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 @@
Copyright 1995 TU Muenchen
*)
-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 @@
Copyright 2000 TU Muenchen
*)
-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 @@
Copyright 1998 TU Muenchen
*)
-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 @@
Copyright 1998 TU Muenchen
*)
-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 @@
Copyright 1998 TU Muenchen
*)
-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 @@
Copyright 2005 TU Muenchen
*)
-header {* Standardization *}
+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 @@
Copyright 2000 TU Muenchen
*)
-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 @@
Copyright 2003 TU Muenchen
*)
-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 @@
Copyright 2012 TU Muenchen
*)
-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 @@
Copyright 2011 TU Muenchen
*)
-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 *)
-header {* The Random-Predicate Monad *}
+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 *)
-header {* Various kind of sequences inside the random monad *}
+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
*)
-header {* Rational numbers *}
+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 @@
Author: Jeremy Avigad
*)
-header {* Rings *}
+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
*)
-header{*The SET Cardholder Registration Protocol*}
+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
*)
-header{*Theory of Events for SET*}
+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
*)
-header{*The SET Merchant Registration Protocol*}
+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
*)
-header{*Purchase Phase of SET*}
+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
*)
-header {* Semiring normalization *}
+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 @@
Additional contributions by Jeremy Avigad
*)
-header {* Infinite Series *}
+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 = {_ ..}
*)
-header {* Set intervals *}
+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
*)
-header {* Sledgehammer: Isabelle--ATP Linkup *}
+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
*)
-header {* Examples \label{sec:Examples} *}
+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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright: 1998 University of Munich
*)
-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 @@
Copyright: 1998 University of Munich
*)
-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 @@
Copyright: 1998 University of Munich
*)
-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 @@
Copyright: 1998 University of Munich
*)
-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
*)
-header {* MaSh Exporter *}
+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
*)
-header {* Taylor series *}
+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
*)
-header {* Topological Spaces *}
+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 @@
Author: Jeremy Avigad
*)
-header{*Power Series, Transcendental Functions etc.*}
+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 @@
Copyright 1992 University of Cambridge
*)
-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.
*)
-header{*Composition: Basic Primitives*}
+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 @@
Copyright 1998 University of Cambridge
*)
-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 @@
Copyright 1998 University of Cambridge
*)
-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 @@
Copyright 1998 University of Cambridge
*)
-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 @@
Copyright 2001 University of Cambridge
*)
-header{*The priority system*}
+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
*)
-header{*Progress Set Examples*}
+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.
*)
-header{*Weak Safety*}
+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
*)
-header{*The Detects Relation*}
+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
*)
-header{*Progress Under Allowable Sets*}
+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"
*)
-header{*Extending State Sets*}
+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
*)
-header{*Fixed Point of a Program*}
+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 @@
Copyright 1998 University of Cambridge
*)
-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.
*)
-header{*Guarantees Specifications*}
+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.
*)
-header{*Replication of Components*}
+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)
*)
-header{*Progress Sets*}
+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.
*)
-header{*Projections of State Sets*}
+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 @@
Copyright 2000 University of Cambridge
*)
-header{*Renaming of State Sets*}
+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 @@
Original file is ../Auth/NS_Public_Bad
*)
-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 @@
*)
-header {*The Token Ring*}
+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)
*)
-header{*Weak Progress*}
+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)
*)
-header{*Predicate Transformers*}
+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.
*)
-header {*The Basic UNITY Theory*}
+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 @@
Copyright 2003 University of Cambridge
*)
-header{*Comprehensive UNITY Theory*}
+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.
*)
-header{*Unions 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
*)
-header{*Progress*}
+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
*)
-header \<open>Nested environments\<close>
+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
*)
-header \<open>Unix file-systems \label{sec:unix-file-system}\<close>
+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
*)
-header {*Well-founded Recursion*}
+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 @@
Author: Konrad Slind
*)
-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.
*)
-header {* Zorn's Lemma *}
+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
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Christian Sternagel
*)
-header {* Ad Hoc Overloading *}
+section {* Ad Hoc Overloading *}
theory Adhoc_Overloading_Examples
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
*)
-header {* Antiquotations *}
+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
*)
-header {* Arithmetic *}
+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
*)
-header {* 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 @@
Copyright 1998 University of Cambridge
*)
-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
*)
-header {* A Formulation of the Birthday Paradox *}
+section {* A Formulation of the Birthday Paradox *}
theory 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 *)
-header {* Bubblesort *}
+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
*)
-header {* CTL formulae *}
+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 @@
Copyright 2011 TU Muenchen
*)
-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 @@
Copyright 1994 University of Cambridge
*)
-header{*Classical Predicate Calculus Problems*}
+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 *)
-header {*
+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
*)
-header {* Examples for hexadecimal and binary numerals *}
+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 @@
Copyright 1996 TU Muenchen
*)
-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 @@
Copyright 2011 TU Muenchen
*)
-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
*)
-header \<open>Isabelle/ML basics\<close>
+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 @@
Copyright 2002 TU Muenchen
*)
-header{*Merge Sort*}
+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 @@
Copyright 1994 TU Muenchen
*)
-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 @@
Copyright 2005-2009
*)
-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
*)
-header \<open>Finite sequences\<close>
+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 @@
Copyright 2012 TU Muenchen
*)
-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 @@
Copyright 1991 University of Cambridge
*)
-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 @@
Copyright 2001 University of Cambridge
*)
-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 @@
Copyright 2005-2014
*)
-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
*)
-header {* 2-3 Trees *}
+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 @@
Copyright 2000 TU Muenchen
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
-header {* Section 10.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 @@
-header {* Example 3.8 *}
+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 @@
-header {* Addition with fixpoint of successor *}
+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 @@
-header {* Prefixpoints *}
+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 @@
Copyright 1999 University of Cambridge
*)
-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 @@
Copyright 1992 University of Cambridge
*)
-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 @@
Copyright 1993 University of Cambridge
*)
-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
+++ b/src/Tools/Adhoc_Overloading.thy Sun Nov 02 18:21:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Christian Sternagel, University of Innsbruck
*)
-header {* Adhoc overloading of constants based on their types *}
+section {* Adhoc overloading of constants based on their types *}
theory Adhoc_Overloading
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
*)
-header {* Loading the code generator and related modules *}
+section {* Loading the code generator and related modules *}
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