--- a/src/HOL/Library/AList.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/AList.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
*)
-header {* Implementation of Association Lists *}
+section {* Implementation of Association Lists *}
theory AList
imports Main
--- a/src/HOL/Library/AList_Mapping.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/AList_Mapping.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Implementation of mappings with Association Lists *}
+section {* Implementation of mappings with Association Lists *}
theory AList_Mapping
imports AList Mapping
--- a/src/HOL/Library/BNF_Axiomatization.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
Axiomatic declaration of bounded natural functors.
*)
-header {* Axiomatic declaration of Bounded Natural Functors *}
+section {* Axiomatic declaration of Bounded Natural Functors *}
theory BNF_Axiomatization
imports Main
--- a/src/HOL/Library/BigO.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/BigO.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Authors: Jeremy Avigad and Kevin Donnelly
*)
-header {* Big O notation *}
+section {* Big O notation *}
theory BigO
imports Complex_Main Function_Algebras Set_Algebras
--- a/src/HOL/Library/Bit.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Bit.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* The Field of Integers mod 2 *}
+section {* The Field of Integers mod 2 *}
theory Bit
imports Main
--- a/src/HOL/Library/Boolean_Algebra.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* Boolean Algebras *}
+section {* Boolean Algebras *}
theory Boolean_Algebra
imports Main
--- a/src/HOL/Library/Cardinal_Notations.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Cardinal_Notations.thy Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
Cardinal notations.
*)
-header {* Cardinal Notations *}
+section {* Cardinal Notations *}
theory Cardinal_Notations
imports Main
--- a/src/HOL/Library/Cardinality.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Cardinality.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman, Andreas Lochbihler
*)
-header {* Cardinality of types *}
+section {* Cardinality of types *}
theory Cardinality
imports Phantom_Type
--- a/src/HOL/Library/Char_ord.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Char_ord.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Norbert Voelker, Florian Haftmann
*)
-header {* Order on characters *}
+section {* Order on characters *}
theory Char_ord
imports Main
--- a/src/HOL/Library/Code_Abstract_Nat.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
*)
-header {* Avoidance of pattern matching on natural numbers *}
+section {* Avoidance of pattern matching on natural numbers *}
theory Code_Abstract_Nat
imports Main
--- a/src/HOL/Library/Code_Binary_Nat.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Implementation of natural numbers as binary numerals *}
+section {* Implementation of natural numbers as binary numerals *}
theory Code_Binary_Nat
imports Code_Abstract_Nat
--- a/src/HOL/Library/Code_Char.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Char.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann
*)
-header {* Code generation of pretty characters (and strings) *}
+section {* Code generation of pretty characters (and strings) *}
theory Code_Char
imports Main Char_ord
--- a/src/HOL/Library/Code_Prolog.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Prolog.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn, TUM 2010
*)
-header {* Code generation of prolog programs *}
+section {* Code generation of prolog programs *}
theory Code_Prolog
imports Main
--- a/src/HOL/Library/Code_Target_Int.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Implementation of integer numbers by target-language integers *}
+section {* Implementation of integer numbers by target-language integers *}
theory Code_Target_Int
imports Main
--- a/src/HOL/Library/Code_Target_Nat.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Implementation of natural numbers by target-language integers *}
+section {* Implementation of natural numbers by target-language integers *}
theory Code_Target_Nat
imports Code_Abstract_Nat
--- a/src/HOL/Library/Code_Target_Numeral.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Code_Target_Numeral.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Implementation of natural and integer numbers by target-language integers *}
+section {* Implementation of natural and integer numbers by target-language integers *}
theory Code_Target_Numeral
imports Code_Target_Int Code_Target_Nat
--- a/src/HOL/Library/ContNotDenum.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Johannes Hölzl, TU München
*)
-header {* Non-denumerability of the Continuum. *}
+section {* Non-denumerability of the Continuum. *}
theory ContNotDenum
imports Complex_Main Countable_Set
--- a/src/HOL/Library/Convex.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Convex.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Johannes Hoelzl, TU Muenchen
*)
-header {* Convexity in real vector spaces *}
+section {* Convexity in real vector spaces *}
theory Convex
imports Product_Vector
--- a/src/HOL/Library/Countable.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Countable.thy Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
Author: Jasmin Blanchette, TU Muenchen
*)
-header {* Encoding (almost) everything into natural numbers *}
+section {* Encoding (almost) everything into natural numbers *}
theory Countable
imports Old_Datatype Rat Nat_Bijection
--- a/src/HOL/Library/Countable_Set.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Countable_Set.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Andrei Popescu
*)
-header {* Countable sets *}
+section {* Countable sets *}
theory Countable_Set
imports Countable Infinite_Set
--- a/src/HOL/Library/Countable_Set_Type.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
Type of (at most) countable sets.
*)
-header {* Type of (at Most) Countable Sets *}
+section {* Type of (at Most) Countable Sets *}
theory Countable_Set_Type
imports Countable_Set Cardinal_Notations
--- a/src/HOL/Library/DAList.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/DAList.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn, TU Muenchen
*)
-header \<open>Abstract type of association lists with unique keys\<close>
+section \<open>Abstract type of association lists with unique keys\<close>
theory DAList
imports AList
--- a/src/HOL/Library/DAList_Multiset.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn, TU Muenchen
*)
-header \<open>Multisets partially implemented by association lists\<close>
+section \<open>Multisets partially implemented by association lists\<close>
theory DAList_Multiset
imports Multiset DAList
--- a/src/HOL/Library/Debug.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Debug.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Debugging facilities for code generated towards Isabelle/ML *}
+section {* Debugging facilities for code generated towards Isabelle/ML *}
theory Debug
imports Main
--- a/src/HOL/Library/Diagonal_Subsequence.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Fabian Immler, TUM *)
-header {* Sequence of Properties on Subsequences *}
+section {* Sequence of Properties on Subsequences *}
theory Diagonal_Subsequence
imports Complex_Main
--- a/src/HOL/Library/Discrete.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Discrete.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Common discrete functions *}
+section {* Common discrete functions *}
theory Discrete
imports Main
--- a/src/HOL/Library/Dlist.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Dlist.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Lists with elements distinct as canonical example for datatype invariants *}
+section {* Lists with elements distinct as canonical example for datatype invariants *}
theory Dlist
imports Main
--- a/src/HOL/Library/Extended_Nat.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Contributions: David Trachtenherz, TU Muenchen
*)
-header {* Extended natural numbers (i.e. with infinity) *}
+section {* Extended natural numbers (i.e. with infinity) *}
theory Extended_Nat
imports Main Countable
--- a/src/HOL/Library/Extended_Real.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
Author: Bogdan Grechuk, University of Edinburgh
*)
-header {* Extended real number line *}
+section {* Extended real number line *}
theory Extended_Real
imports Complex_Main Extended_Nat Liminf_Limsup
--- a/src/HOL/Library/FSet.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FSet.thy Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
Author: Andrei Popescu, TU Muenchen
*)
-header {* Type of finite sets defined as a subtype of sets *}
+section {* Type of finite sets defined as a subtype of sets *}
theory FSet
imports Conditionally_Complete_Lattices
--- a/src/HOL/Library/FinFun.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FinFun.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Andreas Lochbihler, Uni Karlsruhe *)
-header {* Almost everywhere constant functions *}
+section {* Almost everywhere constant functions *}
theory FinFun
imports Cardinality
--- a/src/HOL/Library/FinFun_Syntax.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FinFun_Syntax.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Andreas Lochbihler, KIT *)
-header {* Pretty syntax for almost everywhere constant functions *}
+section {* Pretty syntax for almost everywhere constant functions *}
theory FinFun_Syntax
imports FinFun
--- a/src/HOL/Library/Float.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Float.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2012 TU München
*)
-header {* Floating-Point Numbers *}
+section {* Floating-Point Numbers *}
theory Float
imports Complex_Main Lattice_Algebras
--- a/src/HOL/Library/Formal_Power_Series.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb, University of Cambridge
*)
-header{* A formalization of formal power series *}
+section{* A formalization of formal power series *}
theory Formal_Power_Series
imports "~~/src/HOL/Number_Theory/Binomial"
--- a/src/HOL/Library/Fraction_Field.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Fraction_Field.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb, University of Cambridge
*)
-header{* A formalization of the fraction field of any integral domain;
+section{* A formalization of the fraction field of any integral domain;
generalization of theory Rat from int to any integral domain *}
theory Fraction_Field
--- a/src/HOL/Library/Fun_Lexorder.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Fun_Lexorder.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header \<open>Lexical order on functions\<close>
+section \<open>Lexical order on functions\<close>
theory Fun_Lexorder
imports Main
--- a/src/HOL/Library/FuncSet.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/FuncSet.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
*)
-header \<open>Pi and Function Sets\<close>
+section \<open>Pi and Function Sets\<close>
theory FuncSet
imports Hilbert_Choice Main
--- a/src/HOL/Library/Function_Algebras.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Function_Algebras.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
*)
-header {* Pointwise instantiation of functions to algebra type classes *}
+section {* Pointwise instantiation of functions to algebra type classes *}
theory Function_Algebras
imports Main
--- a/src/HOL/Library/Function_Division.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Function_Division.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TUM
*)
-header {* Pointwise instantiation of functions to division *}
+section {* Pointwise instantiation of functions to division *}
theory Function_Division
imports Function_Algebras
--- a/src/HOL/Library/Function_Growth.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Function_Growth.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,7 +1,7 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Comparing growth of functions on natural numbers by a preorder relation *}
+section {* Comparing growth of functions on natural numbers by a preorder relation *}
theory Function_Growth
imports Main Preorder Discrete
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Amine Chaieb, TU Muenchen *)
-header{*Fundamental Theorem of Algebra*}
+section{*Fundamental Theorem of Algebra*}
theory Fundamental_Theorem_Algebra
imports Polynomial Complex_Main
--- a/src/HOL/Library/Groups_Big_Fun.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header \<open>Big sum and product over function bodies\<close>
+section \<open>Big sum and product over function bodies\<close>
theory Groups_Big_Fun
imports
--- a/src/HOL/Library/IArray.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/IArray.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,4 +1,4 @@
-header "Immutable Arrays with Code Generation"
+section "Immutable Arrays with Code Generation"
theory IArray
imports Main
--- a/src/HOL/Library/Indicator_Function.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Johannes Hoelzl (TU Muenchen)
*)
-header {* Indicator Function *}
+section {* Indicator Function *}
theory Indicator_Function
imports Complex_Main
--- a/src/HOL/Library/Infinite_Set.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Stephan Merz
*)
-header {* Infinite Sets and Related Concepts *}
+section {* Infinite Sets and Related Concepts *}
theory Infinite_Set
imports Main
--- a/src/HOL/Library/Inner_Product.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Inner_Product.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* Inner Product Spaces and the Gradient Derivative *}
+section {* Inner Product Spaces and the Gradient Derivative *}
theory Inner_Product
imports "~~/src/HOL/Complex_Main"
--- a/src/HOL/Library/Lattice_Algebras.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Steven Obua, TU Muenchen *)
-header {* Various algebraic structures combined with a lattice *}
+section {* Various algebraic structures combined with a lattice *}
theory Lattice_Algebras
imports Complex_Main
--- a/src/HOL/Library/Lattice_Syntax.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Pretty syntax for lattice operations *}
+section {* Pretty syntax for lattice operations *}
theory Lattice_Syntax
imports Complete_Lattices
--- a/src/HOL/Library/Liminf_Limsup.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Johannes Hölzl, TU München
*)
-header {* Liminf and Limsup on complete lattices *}
+section {* Liminf and Limsup on complete lattices *}
theory Liminf_Limsup
imports Complex_Main
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Dmitriy Traytel, TU Muenchen
*)
-header {* Linear Temporal Logic on Streams *}
+section {* Linear Temporal Logic on Streams *}
theory Linear_Temporal_Logic_on_Streams
imports Stream Sublist
--- a/src/HOL/Library/ListVector.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/ListVector.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow, 2007 *)
-header {* Lists as vectors *}
+section {* Lists as vectors *}
theory ListVector
imports List Main
--- a/src/HOL/Library/List_lexord.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/List_lexord.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Norbert Voelker
*)
-header {* Lexicographic order on lists *}
+section {* Lexicographic order on lists *}
theory List_lexord
imports Main
--- a/src/HOL/Library/Lub_Glb.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Lub_Glb.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Jacques D. Fleuriot, University of Cambridge
Author: Amine Chaieb, University of Cambridge *)
-header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
+section {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
theory Lub_Glb
imports Complex_Main
--- a/src/HOL/Library/Mapping.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Mapping.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann and Ondrej Kuncar
*)
-header {* An abstract view on maps for code generation. *}
+section {* An abstract view on maps for code generation. *}
theory Mapping
imports Main
--- a/src/HOL/Library/Monad_Syntax.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Christian Sternagel, University of Innsbruck
*)
-header {* Monad notation for arbitrary types *}
+section {* Monad notation for arbitrary types *}
theory Monad_Syntax
imports Main "~~/src/Tools/Adhoc_Overloading"
--- a/src/HOL/Library/More_List.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/More_List.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,7 +1,7 @@
(* Author: Andreas Lochbihler, ETH Zürich
Author: Florian Haftmann, TU Muenchen *)
-header \<open>Less common functions on lists\<close>
+section \<open>Less common functions on lists\<close>
theory More_List
imports Main
--- a/src/HOL/Library/Multiset.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Andrei Popescu, TU Muenchen
*)
-header {* (Finite) multisets *}
+section {* (Finite) multisets *}
theory Multiset
imports Main
--- a/src/HOL/Library/Nat_Bijection.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy Sun Nov 02 17:20:45 2014 +0100
@@ -6,7 +6,7 @@
Author: Alexander Krauss
*)
-header {* Bijections between natural numbers and other types *}
+section {* Bijections between natural numbers and other types *}
theory Nat_Bijection
imports Main
--- a/src/HOL/Library/Numeral_Type.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* Numeral Syntax for Types *}
+section {* Numeral Syntax for Types *}
theory Numeral_Type
imports Cardinality
--- a/src/HOL/Library/Old_Datatype.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Old_Datatype.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
*)
-header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
+section {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
theory Old_Datatype
imports "../Main"
--- a/src/HOL/Library/Old_Recdef.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Konrad Slind and Markus Wenzel, TU Muenchen
*)
-header {* TFL: recursive function definitions *}
+section {* TFL: recursive function definitions *}
theory Old_Recdef
imports Main
--- a/src/HOL/Library/Old_SMT.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Old_SMT.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Sascha Boehme, TU Muenchen
*)
-header {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
+section {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
theory Old_SMT
imports "../Real" "../Word/Word"
--- a/src/HOL/Library/Option_ord.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Option_ord.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Canonical order on option type *}
+section {* Canonical order on option type *}
theory Option_ord
imports Option Main
--- a/src/HOL/Library/Order_Continuity.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Order_Continuity.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb, TU Muenchen
*)
-header {* Continuity and iterations (of set transformers) *}
+section {* Continuity and iterations (of set transformers) *}
theory Order_Continuity
imports Main
--- a/src/HOL/Library/Parallel.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Parallel.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Futures and parallel lists for code generated towards Isabelle/ML *}
+section {* Futures and parallel lists for code generated towards Isabelle/ML *}
theory Parallel
imports Main
--- a/src/HOL/Library/Permutation.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Permutation.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
*)
-header {* Permutations *}
+section {* Permutations *}
theory Permutation
imports Multiset
--- a/src/HOL/Library/Permutations.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Permutations.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb, University of Cambridge
*)
-header {* Permutations, both general and specifically on finite sets.*}
+section {* Permutations, both general and specifically on finite sets.*}
theory Permutations
imports Fact
--- a/src/HOL/Library/Phantom_Type.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Phantom_Type.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Andreas Lochbihler
*)
-header {* A generic phantom type *}
+section {* A generic phantom type *}
theory Phantom_Type
imports Main
--- a/src/HOL/Library/Poly_Deriv.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Brian Huffman
*)
-header{* Polynomials and Differentiation *}
+section{* Polynomials and Differentiation *}
theory Poly_Deriv
imports Deriv Polynomial
--- a/src/HOL/Library/Polynomial.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
Author: Florian Haftmann
*)
-header {* Polynomials as type over a ring structure *}
+section {* Polynomials as type over a ring structure *}
theory Polynomial
imports Main GCD "~~/src/HOL/Library/More_List"
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Lukas Bulwahn, TU Muenchen *)
-header {* A Prototype of Quickcheck based on the Predicate Compiler *}
+section {* A Prototype of Quickcheck based on the Predicate Compiler *}
theory Predicate_Compile_Quickcheck
imports Main Predicate_Compile_Alternative_Defs
--- a/src/HOL/Library/Prefix_Order.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Prefix_Order.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
*)
-header {* Prefix order on lists as order class instance *}
+section {* Prefix order on lists as order class instance *}
theory Prefix_Order
imports Sublist
--- a/src/HOL/Library/Preorder.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Preorder.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Preorders with explicit equivalence relation *}
+section {* Preorders with explicit equivalence relation *}
theory Preorder
imports Orderings
--- a/src/HOL/Library/Product_Lexorder.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_Lexorder.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Norbert Voelker
*)
-header {* Lexicographic order on product types *}
+section {* Lexicographic order on product types *}
theory Product_Lexorder
imports Main
--- a/src/HOL/Library/Product_Order.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* Pointwise order on product types *}
+section {* Pointwise order on product types *}
theory Product_Order
imports Product_plus Conditionally_Complete_Lattices
--- a/src/HOL/Library/Product_Vector.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_Vector.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* Cartesian Products as Vector Spaces *}
+section {* Cartesian Products as Vector Spaces *}
theory Product_Vector
imports Inner_Product Product_plus
--- a/src/HOL/Library/Product_plus.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Product_plus.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-header {* Additive group operations on product types *}
+section {* Additive group operations on product types *}
theory Product_plus
imports Main
--- a/src/HOL/Library/Quotient_List.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_List.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk and Christian Urban
*)
-header {* Quotient infrastructure for the list type *}
+section {* Quotient infrastructure for the list type *}
theory Quotient_List
imports Main Quotient_Set Quotient_Product Quotient_Option
--- a/src/HOL/Library/Quotient_Option.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk and Christian Urban
*)
-header {* Quotient infrastructure for the option type *}
+section {* Quotient infrastructure for the option type *}
theory Quotient_Option
imports Main Quotient_Syntax
--- a/src/HOL/Library/Quotient_Product.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk and Christian Urban
*)
-header {* Quotient infrastructure for the product type *}
+section {* Quotient infrastructure for the product type *}
theory Quotient_Product
imports Main Quotient_Syntax
--- a/src/HOL/Library/Quotient_Set.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Set.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk and Christian Urban
*)
-header {* Quotient infrastructure for the set type *}
+section {* Quotient infrastructure for the set type *}
theory Quotient_Set
imports Main Quotient_Syntax
--- a/src/HOL/Library/Quotient_Sum.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk and Christian Urban
*)
-header {* Quotient infrastructure for the sum type *}
+section {* Quotient infrastructure for the sum type *}
theory Quotient_Sum
imports Main Quotient_Syntax
--- a/src/HOL/Library/Quotient_Syntax.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk and Christian Urban
*)
-header {* Pretty syntax for Quotient operations *}
+section {* Pretty syntax for Quotient operations *}
theory Quotient_Syntax
imports Main
--- a/src/HOL/Library/Quotient_Type.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Quotient_Type.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-header {* Quotient types *}
+section {* Quotient types *}
theory Quotient_Type
imports Main
--- a/src/HOL/Library/RBT.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn and Ondrej Kuncar
*)
-header {* Abstract type of RBT trees *}
+section {* Abstract type of RBT trees *}
theory RBT
imports Main RBT_Impl
--- a/src/HOL/Library/RBT_Impl.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Alexander Krauss, TU Muenchen
*)
-header {* Implementation of Red-Black Trees *}
+section {* Implementation of Red-Black Trees *}
theory RBT_Impl
imports Main
--- a/src/HOL/Library/RBT_Mapping.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann and Ondrej Kuncar
*)
-header {* Implementation of mappings with Red-Black Trees *}
+section {* Implementation of mappings with Red-Black Trees *}
(*<*)
theory RBT_Mapping
--- a/src/HOL/Library/RBT_Set.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Ondrej Kuncar
*)
-header {* Implementation of sets using RBT trees *}
+section {* Implementation of sets using RBT trees *}
theory RBT_Set
imports RBT Product_Lexorder
--- a/src/HOL/Library/Ramsey.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Ramsey.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Tom Ridge. Converted to structured Isar by L C Paulson
*)
-header "Ramsey's Theorem"
+section "Ramsey's Theorem"
theory Ramsey
imports Main Infinite_Set
--- a/src/HOL/Library/Reflection.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Reflection.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb, TU Muenchen
*)
-header {* Generic reflection and reification *}
+section {* Generic reflection and reification *}
theory Reflection
imports Main
--- a/src/HOL/Library/Refute.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Refute.thy Sun Nov 02 17:20:45 2014 +0100
@@ -5,7 +5,7 @@
Basic setup and documentation for the 'refute' (and 'refute_params') command.
*)
-header {* Refute *}
+section {* Refute *}
theory Refute
imports Main
--- a/src/HOL/Library/Saturated.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Saturated.thy Sun Nov 02 17:20:45 2014 +0100
@@ -4,7 +4,7 @@
Author: Florian Haftmann
*)
-header {* Saturated arithmetic *}
+section {* Saturated arithmetic *}
theory Saturated
imports Numeral_Type "~~/src/HOL/Word/Type_Length"
--- a/src/HOL/Library/Set_Algebras.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Set_Algebras.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
*)
-header {* Algebraic operations on sets *}
+section {* Algebraic operations on sets *}
theory Set_Algebras
imports Main
--- a/src/HOL/Library/State_Monad.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/State_Monad.thy Sun Nov 02 17:20:45 2014 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
+section {* Combinator syntax for generic, open state monads (single-threaded monads) *}
theory State_Monad
imports Main Monad_Syntax
--- a/src/HOL/Library/Stream.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Stream.thy Sun Nov 02 17:20:45 2014 +0100
@@ -6,7 +6,7 @@
Infinite streams.
*)
-header {* Infinite Streams *}
+section {* Infinite Streams *}
theory Stream
imports "~~/src/HOL/Library/Nat_Bijection"
--- a/src/HOL/Library/Sublist.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sublist.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Christian Sternagel, JAIST
*)
-header {* List prefixes, suffixes, and homeomorphic embedding *}
+section {* List prefixes, suffixes, and homeomorphic embedding *}
theory Sublist
imports Main
--- a/src/HOL/Library/Sublist_Order.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sublist_Order.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Florian Haftmann, Tobias Nipkow, TU Muenchen
*)
-header {* Sublist Ordering *}
+section {* Sublist Ordering *}
theory Sublist_Order
imports Sublist
--- a/src/HOL/Library/Sum_of_Squares.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Philipp Meyer, TU Muenchen
*)
-header {* A decision procedure for universal multivariate real arithmetic
+section {* A decision procedure for universal multivariate real arithmetic
with addition, multiplication and ordering using semidefinite programming *}
theory Sum_of_Squares
--- a/src/HOL/Library/Sum_of_Squares_Remote.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Sum_of_Squares_Remote.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Philipp Meyer, TU Muenchen
*)
-header {* Examples with remote CSDP *}
+section {* Examples with remote CSDP *}
theory Sum_of_Squares_Remote
imports Sum_of_Squares
--- a/src/HOL/Library/Transitive_Closure_Table.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
-header {* A table-based implementation of the reflexive transitive closure *}
+section {* A table-based implementation of the reflexive transitive closure *}
theory Transitive_Closure_Table
imports Main
--- a/src/HOL/Library/Tree.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/Tree.thy Sun Nov 02 17:20:45 2014 +0100
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)
-header {* Binary Tree *}
+section {* Binary Tree *}
theory Tree
imports Main
--- a/src/HOL/Library/While_Combinator.thy Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/While_Combinator.thy Sun Nov 02 17:20:45 2014 +0100
@@ -3,7 +3,7 @@
Author: Alexander Krauss
*)
-header {* A general ``while'' combinator *}
+section {* A general ``while'' combinator *}
theory While_Combinator
imports Main
--- a/src/HOL/Library/document/root.tex Sun Nov 02 17:16:01 2014 +0100
+++ b/src/HOL/Library/document/root.tex Sun Nov 02 17:20:45 2014 +0100
@@ -18,9 +18,7 @@
\tableofcontents
\newpage
-\renewcommand{\isamarkupheader}[1]%
-{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
-\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
\input{session}