modernized header;
authorwenzelm
Sun Nov 02 17:20:45 2014 +0100 (2014-11-02)
changeset 58881b9556a055632
parent 58880 0baae4311a9f
child 58882 6e2010ab8bd9
modernized header;
src/HOL/Library/AList.thy
src/HOL/Library/AList_Mapping.thy
src/HOL/Library/BNF_Axiomatization.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Cardinal_Notations.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/Code_Binary_Nat.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Prolog.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/Code_Target_Numeral.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/DAList.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Debug.thy
src/HOL/Library/Diagonal_Subsequence.thy
src/HOL/Library/Discrete.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/FinFun_Syntax.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Fun_Lexorder.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Function_Division.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/IArray.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Lattice_Algebras.thy
src/HOL/Library/Lattice_Syntax.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Lub_Glb.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Monad_Syntax.thy
src/HOL/Library/More_List.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/Library/Old_SMT.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Library/Parallel.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Phantom_Type.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Library/Prefix_Order.thy
src/HOL/Library/Preorder.thy
src/HOL/Library/Product_Lexorder.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Product_plus.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Library/Quotient_Syntax.thy
src/HOL/Library/Quotient_Type.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/RBT_Mapping.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/Refute.thy
src/HOL/Library/Saturated.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Stream.thy
src/HOL/Library/Sublist.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Sum_of_Squares.thy
src/HOL/Library/Sum_of_Squares_Remote.thy
src/HOL/Library/Transitive_Closure_Table.thy
src/HOL/Library/Tree.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/document/root.tex
     1.1 --- a/src/HOL/Library/AList.thy	Sun Nov 02 17:16:01 2014 +0100
     1.2 +++ b/src/HOL/Library/AList.thy	Sun Nov 02 17:20:45 2014 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
     1.5  *)
     1.6  
     1.7 -header {* Implementation of Association Lists *}
     1.8 +section {* Implementation of Association Lists *}
     1.9  
    1.10  theory AList
    1.11  imports Main
     2.1 --- a/src/HOL/Library/AList_Mapping.thy	Sun Nov 02 17:16:01 2014 +0100
     2.2 +++ b/src/HOL/Library/AList_Mapping.thy	Sun Nov 02 17:20:45 2014 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4     Author: Florian Haftmann, TU Muenchen
     2.5  *)
     2.6  
     2.7 -header {* Implementation of mappings with Association Lists *}
     2.8 +section {* Implementation of mappings with Association Lists *}
     2.9  
    2.10  theory AList_Mapping
    2.11  imports AList Mapping
     3.1 --- a/src/HOL/Library/BNF_Axiomatization.thy	Sun Nov 02 17:16:01 2014 +0100
     3.2 +++ b/src/HOL/Library/BNF_Axiomatization.thy	Sun Nov 02 17:20:45 2014 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  Axiomatic declaration of bounded natural functors.
     3.5  *)
     3.6  
     3.7 -header {* Axiomatic declaration of Bounded Natural Functors *}
     3.8 +section {* Axiomatic declaration of Bounded Natural Functors *}
     3.9  
    3.10  theory BNF_Axiomatization
    3.11  imports Main
     4.1 --- a/src/HOL/Library/BigO.thy	Sun Nov 02 17:16:01 2014 +0100
     4.2 +++ b/src/HOL/Library/BigO.thy	Sun Nov 02 17:20:45 2014 +0100
     4.3 @@ -2,7 +2,7 @@
     4.4      Authors:    Jeremy Avigad and Kevin Donnelly
     4.5  *)
     4.6  
     4.7 -header {* Big O notation *}
     4.8 +section {* Big O notation *}
     4.9  
    4.10  theory BigO
    4.11  imports Complex_Main Function_Algebras Set_Algebras
     5.1 --- a/src/HOL/Library/Bit.thy	Sun Nov 02 17:16:01 2014 +0100
     5.2 +++ b/src/HOL/Library/Bit.thy	Sun Nov 02 17:20:45 2014 +0100
     5.3 @@ -2,7 +2,7 @@
     5.4      Author:     Brian Huffman
     5.5  *)
     5.6  
     5.7 -header {* The Field of Integers mod 2 *}
     5.8 +section {* The Field of Integers mod 2 *}
     5.9  
    5.10  theory Bit
    5.11  imports Main
     6.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Sun Nov 02 17:16:01 2014 +0100
     6.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Sun Nov 02 17:20:45 2014 +0100
     6.3 @@ -2,7 +2,7 @@
     6.4      Author:     Brian Huffman
     6.5  *)
     6.6  
     6.7 -header {* Boolean Algebras *}
     6.8 +section {* Boolean Algebras *}
     6.9  
    6.10  theory Boolean_Algebra
    6.11  imports Main
     7.1 --- a/src/HOL/Library/Cardinal_Notations.thy	Sun Nov 02 17:16:01 2014 +0100
     7.2 +++ b/src/HOL/Library/Cardinal_Notations.thy	Sun Nov 02 17:20:45 2014 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  Cardinal notations.
     7.5  *)
     7.6  
     7.7 -header {* Cardinal Notations *}
     7.8 +section {* Cardinal Notations *}
     7.9  
    7.10  theory Cardinal_Notations
    7.11  imports Main
     8.1 --- a/src/HOL/Library/Cardinality.thy	Sun Nov 02 17:16:01 2014 +0100
     8.2 +++ b/src/HOL/Library/Cardinality.thy	Sun Nov 02 17:20:45 2014 +0100
     8.3 @@ -2,7 +2,7 @@
     8.4      Author:     Brian Huffman, Andreas Lochbihler
     8.5  *)
     8.6  
     8.7 -header {* Cardinality of types *}
     8.8 +section {* Cardinality of types *}
     8.9  
    8.10  theory Cardinality
    8.11  imports Phantom_Type
     9.1 --- a/src/HOL/Library/Char_ord.thy	Sun Nov 02 17:16:01 2014 +0100
     9.2 +++ b/src/HOL/Library/Char_ord.thy	Sun Nov 02 17:20:45 2014 +0100
     9.3 @@ -2,7 +2,7 @@
     9.4      Author:     Norbert Voelker, Florian Haftmann
     9.5  *)
     9.6  
     9.7 -header {* Order on characters *}
     9.8 +section {* Order on characters *}
     9.9  
    9.10  theory Char_ord
    9.11  imports Main
    10.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
    10.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
    10.3 @@ -2,7 +2,7 @@
    10.4      Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
    10.5  *)
    10.6  
    10.7 -header {* Avoidance of pattern matching on natural numbers *}
    10.8 +section {* Avoidance of pattern matching on natural numbers *}
    10.9  
   10.10  theory Code_Abstract_Nat
   10.11  imports Main
    11.1 --- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
    11.2 +++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
    11.3 @@ -2,7 +2,7 @@
    11.4      Author:     Florian Haftmann, TU Muenchen
    11.5  *)
    11.6  
    11.7 -header {* Implementation of natural numbers as binary numerals *}
    11.8 +section {* Implementation of natural numbers as binary numerals *}
    11.9  
   11.10  theory Code_Binary_Nat
   11.11  imports Code_Abstract_Nat
    12.1 --- a/src/HOL/Library/Code_Char.thy	Sun Nov 02 17:16:01 2014 +0100
    12.2 +++ b/src/HOL/Library/Code_Char.thy	Sun Nov 02 17:20:45 2014 +0100
    12.3 @@ -2,7 +2,7 @@
    12.4      Author:     Florian Haftmann
    12.5  *)
    12.6  
    12.7 -header {* Code generation of pretty characters (and strings) *}
    12.8 +section {* Code generation of pretty characters (and strings) *}
    12.9  
   12.10  theory Code_Char
   12.11  imports Main Char_ord
    13.1 --- a/src/HOL/Library/Code_Prolog.thy	Sun Nov 02 17:16:01 2014 +0100
    13.2 +++ b/src/HOL/Library/Code_Prolog.thy	Sun Nov 02 17:20:45 2014 +0100
    13.3 @@ -2,7 +2,7 @@
    13.4      Author:     Lukas Bulwahn, TUM 2010
    13.5  *)
    13.6  
    13.7 -header {* Code generation of prolog programs *}
    13.8 +section {* Code generation of prolog programs *}
    13.9  
   13.10  theory Code_Prolog
   13.11  imports Main
    14.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sun Nov 02 17:16:01 2014 +0100
    14.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sun Nov 02 17:20:45 2014 +0100
    14.3 @@ -2,7 +2,7 @@
    14.4      Author:     Florian Haftmann, TU Muenchen
    14.5  *)
    14.6  
    14.7 -header {* Implementation of integer numbers by target-language integers *}
    14.8 +section {* Implementation of integer numbers by target-language integers *}
    14.9  
   14.10  theory Code_Target_Int
   14.11  imports Main
    15.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
    15.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
    15.3 @@ -2,7 +2,7 @@
    15.4      Author:     Florian Haftmann, TU Muenchen
    15.5  *)
    15.6  
    15.7 -header {* Implementation of natural numbers by target-language integers *}
    15.8 +section {* Implementation of natural numbers by target-language integers *}
    15.9  
   15.10  theory Code_Target_Nat
   15.11  imports Code_Abstract_Nat
    16.1 --- a/src/HOL/Library/Code_Target_Numeral.thy	Sun Nov 02 17:16:01 2014 +0100
    16.2 +++ b/src/HOL/Library/Code_Target_Numeral.thy	Sun Nov 02 17:20:45 2014 +0100
    16.3 @@ -2,7 +2,7 @@
    16.4      Author:     Florian Haftmann, TU Muenchen
    16.5  *)
    16.6  
    16.7 -header {* Implementation of natural and integer numbers by target-language integers *}
    16.8 +section {* Implementation of natural and integer numbers by target-language integers *}
    16.9  
   16.10  theory Code_Target_Numeral
   16.11  imports Code_Target_Int Code_Target_Nat
    17.1 --- a/src/HOL/Library/ContNotDenum.thy	Sun Nov 02 17:16:01 2014 +0100
    17.2 +++ b/src/HOL/Library/ContNotDenum.thy	Sun Nov 02 17:20:45 2014 +0100
    17.3 @@ -3,7 +3,7 @@
    17.4      Author:     Johannes Hölzl, TU München
    17.5  *)
    17.6  
    17.7 -header {* Non-denumerability of the Continuum. *}
    17.8 +section {* Non-denumerability of the Continuum. *}
    17.9  
   17.10  theory ContNotDenum
   17.11  imports Complex_Main Countable_Set
    18.1 --- a/src/HOL/Library/Convex.thy	Sun Nov 02 17:16:01 2014 +0100
    18.2 +++ b/src/HOL/Library/Convex.thy	Sun Nov 02 17:20:45 2014 +0100
    18.3 @@ -3,7 +3,7 @@
    18.4      Author:     Johannes Hoelzl, TU Muenchen
    18.5  *)
    18.6  
    18.7 -header {* Convexity in real vector spaces *}
    18.8 +section {* Convexity in real vector spaces *}
    18.9  
   18.10  theory Convex
   18.11  imports Product_Vector
    19.1 --- a/src/HOL/Library/Countable.thy	Sun Nov 02 17:16:01 2014 +0100
    19.2 +++ b/src/HOL/Library/Countable.thy	Sun Nov 02 17:20:45 2014 +0100
    19.3 @@ -4,7 +4,7 @@
    19.4      Author:     Jasmin Blanchette, TU Muenchen
    19.5  *)
    19.6  
    19.7 -header {* Encoding (almost) everything into natural numbers *}
    19.8 +section {* Encoding (almost) everything into natural numbers *}
    19.9  
   19.10  theory Countable
   19.11  imports Old_Datatype Rat Nat_Bijection
    20.1 --- a/src/HOL/Library/Countable_Set.thy	Sun Nov 02 17:16:01 2014 +0100
    20.2 +++ b/src/HOL/Library/Countable_Set.thy	Sun Nov 02 17:20:45 2014 +0100
    20.3 @@ -3,7 +3,7 @@
    20.4      Author:     Andrei Popescu
    20.5  *)
    20.6  
    20.7 -header {* Countable sets *}
    20.8 +section {* Countable sets *}
    20.9  
   20.10  theory Countable_Set
   20.11  imports Countable Infinite_Set
    21.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 02 17:16:01 2014 +0100
    21.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 02 17:20:45 2014 +0100
    21.3 @@ -5,7 +5,7 @@
    21.4  Type of (at most) countable sets.
    21.5  *)
    21.6  
    21.7 -header {* Type of (at Most) Countable Sets *}
    21.8 +section {* Type of (at Most) Countable Sets *}
    21.9  
   21.10  theory Countable_Set_Type
   21.11  imports Countable_Set Cardinal_Notations
    22.1 --- a/src/HOL/Library/DAList.thy	Sun Nov 02 17:16:01 2014 +0100
    22.2 +++ b/src/HOL/Library/DAList.thy	Sun Nov 02 17:20:45 2014 +0100
    22.3 @@ -2,7 +2,7 @@
    22.4      Author:     Lukas Bulwahn, TU Muenchen
    22.5  *)
    22.6  
    22.7 -header \<open>Abstract type of association lists with unique keys\<close>
    22.8 +section \<open>Abstract type of association lists with unique keys\<close>
    22.9  
   22.10  theory DAList
   22.11  imports AList
    23.1 --- a/src/HOL/Library/DAList_Multiset.thy	Sun Nov 02 17:16:01 2014 +0100
    23.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Sun Nov 02 17:20:45 2014 +0100
    23.3 @@ -2,7 +2,7 @@
    23.4      Author:     Lukas Bulwahn, TU Muenchen
    23.5  *)
    23.6  
    23.7 -header \<open>Multisets partially implemented by association lists\<close>
    23.8 +section \<open>Multisets partially implemented by association lists\<close>
    23.9  
   23.10  theory DAList_Multiset
   23.11  imports Multiset DAList
    24.1 --- a/src/HOL/Library/Debug.thy	Sun Nov 02 17:16:01 2014 +0100
    24.2 +++ b/src/HOL/Library/Debug.thy	Sun Nov 02 17:20:45 2014 +0100
    24.3 @@ -1,6 +1,6 @@
    24.4  (* Author: Florian Haftmann, TU Muenchen *)
    24.5  
    24.6 -header {* Debugging facilities for code generated towards Isabelle/ML *}
    24.7 +section {* Debugging facilities for code generated towards Isabelle/ML *}
    24.8  
    24.9  theory Debug
   24.10  imports Main
    25.1 --- a/src/HOL/Library/Diagonal_Subsequence.thy	Sun Nov 02 17:16:01 2014 +0100
    25.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy	Sun Nov 02 17:20:45 2014 +0100
    25.3 @@ -1,6 +1,6 @@
    25.4  (* Author: Fabian Immler, TUM *)
    25.5  
    25.6 -header {* Sequence of Properties on Subsequences *}
    25.7 +section {* Sequence of Properties on Subsequences *}
    25.8  
    25.9  theory Diagonal_Subsequence
   25.10  imports Complex_Main
    26.1 --- a/src/HOL/Library/Discrete.thy	Sun Nov 02 17:16:01 2014 +0100
    26.2 +++ b/src/HOL/Library/Discrete.thy	Sun Nov 02 17:20:45 2014 +0100
    26.3 @@ -1,6 +1,6 @@
    26.4  (* Author: Florian Haftmann, TU Muenchen *)  
    26.5  
    26.6 -header {* Common discrete functions *}
    26.7 +section {* Common discrete functions *}
    26.8  
    26.9  theory Discrete
   26.10  imports Main
    27.1 --- a/src/HOL/Library/Dlist.thy	Sun Nov 02 17:16:01 2014 +0100
    27.2 +++ b/src/HOL/Library/Dlist.thy	Sun Nov 02 17:20:45 2014 +0100
    27.3 @@ -1,6 +1,6 @@
    27.4  (* Author: Florian Haftmann, TU Muenchen *)
    27.5  
    27.6 -header {* Lists with elements distinct as canonical example for datatype invariants *}
    27.7 +section {* Lists with elements distinct as canonical example for datatype invariants *}
    27.8  
    27.9  theory Dlist
   27.10  imports Main
    28.1 --- a/src/HOL/Library/Extended_Nat.thy	Sun Nov 02 17:16:01 2014 +0100
    28.2 +++ b/src/HOL/Library/Extended_Nat.thy	Sun Nov 02 17:20:45 2014 +0100
    28.3 @@ -3,7 +3,7 @@
    28.4      Contributions: David Trachtenherz, TU Muenchen
    28.5  *)
    28.6  
    28.7 -header {* Extended natural numbers (i.e. with infinity) *}
    28.8 +section {* Extended natural numbers (i.e. with infinity) *}
    28.9  
   28.10  theory Extended_Nat
   28.11  imports Main Countable
    29.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Nov 02 17:16:01 2014 +0100
    29.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun Nov 02 17:20:45 2014 +0100
    29.3 @@ -5,7 +5,7 @@
    29.4      Author:     Bogdan Grechuk, University of Edinburgh
    29.5  *)
    29.6  
    29.7 -header {* Extended real number line *}
    29.8 +section {* Extended real number line *}
    29.9  
   29.10  theory Extended_Real
   29.11  imports Complex_Main Extended_Nat Liminf_Limsup
    30.1 --- a/src/HOL/Library/FSet.thy	Sun Nov 02 17:16:01 2014 +0100
    30.2 +++ b/src/HOL/Library/FSet.thy	Sun Nov 02 17:20:45 2014 +0100
    30.3 @@ -4,7 +4,7 @@
    30.4      Author:     Andrei Popescu, TU Muenchen
    30.5  *)
    30.6  
    30.7 -header {* Type of finite sets defined as a subtype of sets *}
    30.8 +section {* Type of finite sets defined as a subtype of sets *}
    30.9  
   30.10  theory FSet
   30.11  imports Conditionally_Complete_Lattices
    31.1 --- a/src/HOL/Library/FinFun.thy	Sun Nov 02 17:16:01 2014 +0100
    31.2 +++ b/src/HOL/Library/FinFun.thy	Sun Nov 02 17:20:45 2014 +0100
    31.3 @@ -1,6 +1,6 @@
    31.4  (* Author: Andreas Lochbihler, Uni Karlsruhe *)
    31.5  
    31.6 -header {* Almost everywhere constant functions *}
    31.7 +section {* Almost everywhere constant functions *}
    31.8  
    31.9  theory FinFun
   31.10  imports Cardinality
    32.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
    32.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
    32.3 @@ -1,6 +1,6 @@
    32.4  (* Author: Andreas Lochbihler, KIT *)
    32.5  
    32.6 -header {* Pretty syntax for almost everywhere constant functions *}
    32.7 +section {* Pretty syntax for almost everywhere constant functions *}
    32.8  
    32.9  theory FinFun_Syntax
   32.10  imports FinFun
    33.1 --- a/src/HOL/Library/Float.thy	Sun Nov 02 17:16:01 2014 +0100
    33.2 +++ b/src/HOL/Library/Float.thy	Sun Nov 02 17:20:45 2014 +0100
    33.3 @@ -3,7 +3,7 @@
    33.4      Copyright   2012  TU München
    33.5  *)
    33.6  
    33.7 -header {* Floating-Point Numbers *}
    33.8 +section {* Floating-Point Numbers *}
    33.9  
   33.10  theory Float
   33.11  imports Complex_Main Lattice_Algebras
    34.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Nov 02 17:16:01 2014 +0100
    34.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Nov 02 17:20:45 2014 +0100
    34.3 @@ -2,7 +2,7 @@
    34.4      Author:     Amine Chaieb, University of Cambridge
    34.5  *)
    34.6  
    34.7 -header{* A formalization of formal power series *}
    34.8 +section{* A formalization of formal power series *}
    34.9  
   34.10  theory Formal_Power_Series
   34.11  imports "~~/src/HOL/Number_Theory/Binomial"
    35.1 --- a/src/HOL/Library/Fraction_Field.thy	Sun Nov 02 17:16:01 2014 +0100
    35.2 +++ b/src/HOL/Library/Fraction_Field.thy	Sun Nov 02 17:20:45 2014 +0100
    35.3 @@ -2,7 +2,7 @@
    35.4      Author:     Amine Chaieb, University of Cambridge
    35.5  *)
    35.6  
    35.7 -header{* A formalization of the fraction field of any integral domain;
    35.8 +section{* A formalization of the fraction field of any integral domain;
    35.9           generalization of theory Rat from int to any integral domain *}
   35.10  
   35.11  theory Fraction_Field
    36.1 --- a/src/HOL/Library/Fun_Lexorder.thy	Sun Nov 02 17:16:01 2014 +0100
    36.2 +++ b/src/HOL/Library/Fun_Lexorder.thy	Sun Nov 02 17:20:45 2014 +0100
    36.3 @@ -1,6 +1,6 @@
    36.4  (* Author: Florian Haftmann, TU Muenchen *)
    36.5  
    36.6 -header \<open>Lexical order on functions\<close>
    36.7 +section \<open>Lexical order on functions\<close>
    36.8  
    36.9  theory Fun_Lexorder
   36.10  imports Main
    37.1 --- a/src/HOL/Library/FuncSet.thy	Sun Nov 02 17:16:01 2014 +0100
    37.2 +++ b/src/HOL/Library/FuncSet.thy	Sun Nov 02 17:20:45 2014 +0100
    37.3 @@ -2,7 +2,7 @@
    37.4      Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
    37.5  *)
    37.6  
    37.7 -header \<open>Pi and Function Sets\<close>
    37.8 +section \<open>Pi and Function Sets\<close>
    37.9  
   37.10  theory FuncSet
   37.11  imports Hilbert_Choice Main
    38.1 --- a/src/HOL/Library/Function_Algebras.thy	Sun Nov 02 17:16:01 2014 +0100
    38.2 +++ b/src/HOL/Library/Function_Algebras.thy	Sun Nov 02 17:20:45 2014 +0100
    38.3 @@ -2,7 +2,7 @@
    38.4      Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
    38.5  *)
    38.6  
    38.7 -header {* Pointwise instantiation of functions to algebra type classes *}
    38.8 +section {* Pointwise instantiation of functions to algebra type classes *}
    38.9  
   38.10  theory Function_Algebras
   38.11  imports Main
    39.1 --- a/src/HOL/Library/Function_Division.thy	Sun Nov 02 17:16:01 2014 +0100
    39.2 +++ b/src/HOL/Library/Function_Division.thy	Sun Nov 02 17:20:45 2014 +0100
    39.3 @@ -2,7 +2,7 @@
    39.4      Author:     Florian Haftmann, TUM
    39.5  *)
    39.6  
    39.7 -header {* Pointwise instantiation of functions to division *}
    39.8 +section {* Pointwise instantiation of functions to division *}
    39.9  
   39.10  theory Function_Division
   39.11  imports Function_Algebras
    40.1 --- a/src/HOL/Library/Function_Growth.thy	Sun Nov 02 17:16:01 2014 +0100
    40.2 +++ b/src/HOL/Library/Function_Growth.thy	Sun Nov 02 17:20:45 2014 +0100
    40.3 @@ -1,7 +1,7 @@
    40.4  
    40.5  (* Author: Florian Haftmann, TU Muenchen *)
    40.6  
    40.7 -header {* Comparing growth of functions on natural numbers by a preorder relation *}
    40.8 +section {* Comparing growth of functions on natural numbers by a preorder relation *}
    40.9  
   40.10  theory Function_Growth
   40.11  imports Main Preorder Discrete
    41.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Nov 02 17:16:01 2014 +0100
    41.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Nov 02 17:20:45 2014 +0100
    41.3 @@ -1,6 +1,6 @@
    41.4  (* Author: Amine Chaieb, TU Muenchen *)
    41.5  
    41.6 -header{*Fundamental Theorem of Algebra*}
    41.7 +section{*Fundamental Theorem of Algebra*}
    41.8  
    41.9  theory Fundamental_Theorem_Algebra
   41.10  imports Polynomial Complex_Main
    42.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sun Nov 02 17:16:01 2014 +0100
    42.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Nov 02 17:20:45 2014 +0100
    42.3 @@ -1,6 +1,6 @@
    42.4  (* Author: Florian Haftmann, TU Muenchen *)
    42.5  
    42.6 -header \<open>Big sum and product over function bodies\<close>
    42.7 +section \<open>Big sum and product over function bodies\<close>
    42.8  
    42.9  theory Groups_Big_Fun
   42.10  imports
    43.1 --- a/src/HOL/Library/IArray.thy	Sun Nov 02 17:16:01 2014 +0100
    43.2 +++ b/src/HOL/Library/IArray.thy	Sun Nov 02 17:20:45 2014 +0100
    43.3 @@ -1,4 +1,4 @@
    43.4 -header "Immutable Arrays with Code Generation"
    43.5 +section "Immutable Arrays with Code Generation"
    43.6  
    43.7  theory IArray
    43.8  imports Main
    44.1 --- a/src/HOL/Library/Indicator_Function.thy	Sun Nov 02 17:16:01 2014 +0100
    44.2 +++ b/src/HOL/Library/Indicator_Function.thy	Sun Nov 02 17:20:45 2014 +0100
    44.3 @@ -2,7 +2,7 @@
    44.4      Author:     Johannes Hoelzl (TU Muenchen)
    44.5  *)
    44.6  
    44.7 -header {* Indicator Function *}
    44.8 +section {* Indicator Function *}
    44.9  
   44.10  theory Indicator_Function
   44.11  imports Complex_Main
    45.1 --- a/src/HOL/Library/Infinite_Set.thy	Sun Nov 02 17:16:01 2014 +0100
    45.2 +++ b/src/HOL/Library/Infinite_Set.thy	Sun Nov 02 17:20:45 2014 +0100
    45.3 @@ -2,7 +2,7 @@
    45.4      Author:     Stephan Merz
    45.5  *)
    45.6  
    45.7 -header {* Infinite Sets and Related Concepts *}
    45.8 +section {* Infinite Sets and Related Concepts *}
    45.9  
   45.10  theory Infinite_Set
   45.11  imports Main
    46.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Nov 02 17:16:01 2014 +0100
    46.2 +++ b/src/HOL/Library/Inner_Product.thy	Sun Nov 02 17:20:45 2014 +0100
    46.3 @@ -2,7 +2,7 @@
    46.4      Author:     Brian Huffman
    46.5  *)
    46.6  
    46.7 -header {* Inner Product Spaces and the Gradient Derivative *}
    46.8 +section {* Inner Product Spaces and the Gradient Derivative *}
    46.9  
   46.10  theory Inner_Product
   46.11  imports "~~/src/HOL/Complex_Main"
    47.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Sun Nov 02 17:16:01 2014 +0100
    47.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Sun Nov 02 17:20:45 2014 +0100
    47.3 @@ -1,6 +1,6 @@
    47.4  (* Author: Steven Obua, TU Muenchen *)
    47.5  
    47.6 -header {* Various algebraic structures combined with a lattice *}
    47.7 +section {* Various algebraic structures combined with a lattice *}
    47.8  
    47.9  theory Lattice_Algebras
   47.10  imports Complex_Main
    48.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
    48.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
    48.3 @@ -1,6 +1,6 @@
    48.4  (* Author: Florian Haftmann, TU Muenchen *)
    48.5  
    48.6 -header {* Pretty syntax for lattice operations *}
    48.7 +section {* Pretty syntax for lattice operations *}
    48.8  
    48.9  theory Lattice_Syntax
   48.10  imports Complete_Lattices
    49.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 02 17:16:01 2014 +0100
    49.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 02 17:20:45 2014 +0100
    49.3 @@ -2,7 +2,7 @@
    49.4      Author:     Johannes Hölzl, TU München
    49.5  *)
    49.6  
    49.7 -header {* Liminf and Limsup on complete lattices *}
    49.8 +section {* Liminf and Limsup on complete lattices *}
    49.9  
   49.10  theory Liminf_Limsup
   49.11  imports Complex_Main
    50.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Sun Nov 02 17:16:01 2014 +0100
    50.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Sun Nov 02 17:20:45 2014 +0100
    50.3 @@ -3,7 +3,7 @@
    50.4      Author:     Dmitriy Traytel, TU Muenchen
    50.5  *)
    50.6  
    50.7 -header {* Linear Temporal Logic on Streams *}
    50.8 +section {* Linear Temporal Logic on Streams *}
    50.9  
   50.10  theory Linear_Temporal_Logic_on_Streams
   50.11    imports Stream Sublist
    51.1 --- a/src/HOL/Library/ListVector.thy	Sun Nov 02 17:16:01 2014 +0100
    51.2 +++ b/src/HOL/Library/ListVector.thy	Sun Nov 02 17:20:45 2014 +0100
    51.3 @@ -1,6 +1,6 @@
    51.4  (*  Author: Tobias Nipkow, 2007 *)
    51.5  
    51.6 -header {* Lists as vectors *}
    51.7 +section {* Lists as vectors *}
    51.8  
    51.9  theory ListVector
   51.10  imports List Main
    52.1 --- a/src/HOL/Library/List_lexord.thy	Sun Nov 02 17:16:01 2014 +0100
    52.2 +++ b/src/HOL/Library/List_lexord.thy	Sun Nov 02 17:20:45 2014 +0100
    52.3 @@ -2,7 +2,7 @@
    52.4      Author:     Norbert Voelker
    52.5  *)
    52.6  
    52.7 -header {* Lexicographic order on lists *}
    52.8 +section {* Lexicographic order on lists *}
    52.9  
   52.10  theory List_lexord
   52.11  imports Main
    53.1 --- a/src/HOL/Library/Lub_Glb.thy	Sun Nov 02 17:16:01 2014 +0100
    53.2 +++ b/src/HOL/Library/Lub_Glb.thy	Sun Nov 02 17:20:45 2014 +0100
    53.3 @@ -2,7 +2,7 @@
    53.4      Author:     Jacques D. Fleuriot, University of Cambridge
    53.5      Author:     Amine Chaieb, University of Cambridge *)
    53.6  
    53.7 -header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
    53.8 +section {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
    53.9  
   53.10  theory Lub_Glb
   53.11  imports Complex_Main
    54.1 --- a/src/HOL/Library/Mapping.thy	Sun Nov 02 17:16:01 2014 +0100
    54.2 +++ b/src/HOL/Library/Mapping.thy	Sun Nov 02 17:20:45 2014 +0100
    54.3 @@ -2,7 +2,7 @@
    54.4      Author:     Florian Haftmann and Ondrej Kuncar
    54.5  *)
    54.6  
    54.7 -header {* An abstract view on maps for code generation. *}
    54.8 +section {* An abstract view on maps for code generation. *}
    54.9  
   54.10  theory Mapping
   54.11  imports Main
    55.1 --- a/src/HOL/Library/Monad_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
    55.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
    55.3 @@ -2,7 +2,7 @@
    55.4     Author: Christian Sternagel, University of Innsbruck
    55.5  *)
    55.6  
    55.7 -header {* Monad notation for arbitrary types *}
    55.8 +section {* Monad notation for arbitrary types *}
    55.9  
   55.10  theory Monad_Syntax
   55.11  imports Main "~~/src/Tools/Adhoc_Overloading"
    56.1 --- a/src/HOL/Library/More_List.thy	Sun Nov 02 17:16:01 2014 +0100
    56.2 +++ b/src/HOL/Library/More_List.thy	Sun Nov 02 17:20:45 2014 +0100
    56.3 @@ -1,7 +1,7 @@
    56.4  (* Author: Andreas Lochbihler, ETH Zürich
    56.5     Author: Florian Haftmann, TU Muenchen  *)
    56.6  
    56.7 -header \<open>Less common functions on lists\<close>
    56.8 +section \<open>Less common functions on lists\<close>
    56.9  
   56.10  theory More_List
   56.11  imports Main
    57.1 --- a/src/HOL/Library/Multiset.thy	Sun Nov 02 17:16:01 2014 +0100
    57.2 +++ b/src/HOL/Library/Multiset.thy	Sun Nov 02 17:20:45 2014 +0100
    57.3 @@ -3,7 +3,7 @@
    57.4      Author:     Andrei Popescu, TU Muenchen
    57.5  *)
    57.6  
    57.7 -header {* (Finite) multisets *}
    57.8 +section {* (Finite) multisets *}
    57.9  
   57.10  theory Multiset
   57.11  imports Main
    58.1 --- a/src/HOL/Library/Nat_Bijection.thy	Sun Nov 02 17:16:01 2014 +0100
    58.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Sun Nov 02 17:20:45 2014 +0100
    58.3 @@ -6,7 +6,7 @@
    58.4      Author:     Alexander Krauss
    58.5  *)
    58.6  
    58.7 -header {* Bijections between natural numbers and other types *}
    58.8 +section {* Bijections between natural numbers and other types *}
    58.9  
   58.10  theory Nat_Bijection
   58.11  imports Main
    59.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Nov 02 17:16:01 2014 +0100
    59.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sun Nov 02 17:20:45 2014 +0100
    59.3 @@ -2,7 +2,7 @@
    59.4      Author:     Brian Huffman
    59.5  *)
    59.6  
    59.7 -header {* Numeral Syntax for Types *}
    59.8 +section {* Numeral Syntax for Types *}
    59.9  
   59.10  theory Numeral_Type
   59.11  imports Cardinality
    60.1 --- a/src/HOL/Library/Old_Datatype.thy	Sun Nov 02 17:16:01 2014 +0100
    60.2 +++ b/src/HOL/Library/Old_Datatype.thy	Sun Nov 02 17:20:45 2014 +0100
    60.3 @@ -3,7 +3,7 @@
    60.4      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    60.5  *)
    60.6  
    60.7 -header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
    60.8 +section {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
    60.9  
   60.10  theory Old_Datatype
   60.11  imports "../Main"
    61.1 --- a/src/HOL/Library/Old_Recdef.thy	Sun Nov 02 17:16:01 2014 +0100
    61.2 +++ b/src/HOL/Library/Old_Recdef.thy	Sun Nov 02 17:20:45 2014 +0100
    61.3 @@ -2,7 +2,7 @@
    61.4      Author:     Konrad Slind and Markus Wenzel, TU Muenchen
    61.5  *)
    61.6  
    61.7 -header {* TFL: recursive function definitions *}
    61.8 +section {* TFL: recursive function definitions *}
    61.9  
   61.10  theory Old_Recdef
   61.11  imports Main
    62.1 --- a/src/HOL/Library/Old_SMT.thy	Sun Nov 02 17:16:01 2014 +0100
    62.2 +++ b/src/HOL/Library/Old_SMT.thy	Sun Nov 02 17:20:45 2014 +0100
    62.3 @@ -2,7 +2,7 @@
    62.4      Author:     Sascha Boehme, TU Muenchen
    62.5  *)
    62.6  
    62.7 -header {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
    62.8 +section {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
    62.9  
   62.10  theory Old_SMT
   62.11  imports "../Real" "../Word/Word"
    63.1 --- a/src/HOL/Library/Option_ord.thy	Sun Nov 02 17:16:01 2014 +0100
    63.2 +++ b/src/HOL/Library/Option_ord.thy	Sun Nov 02 17:20:45 2014 +0100
    63.3 @@ -2,7 +2,7 @@
    63.4      Author:     Florian Haftmann, TU Muenchen
    63.5  *)
    63.6  
    63.7 -header {* Canonical order on option type *}
    63.8 +section {* Canonical order on option type *}
    63.9  
   63.10  theory Option_ord
   63.11  imports Option Main
    64.1 --- a/src/HOL/Library/Order_Continuity.thy	Sun Nov 02 17:16:01 2014 +0100
    64.2 +++ b/src/HOL/Library/Order_Continuity.thy	Sun Nov 02 17:20:45 2014 +0100
    64.3 @@ -2,7 +2,7 @@
    64.4      Author:     David von Oheimb, TU Muenchen
    64.5  *)
    64.6  
    64.7 -header {* Continuity and iterations (of set transformers) *}
    64.8 +section {* Continuity and iterations (of set transformers) *}
    64.9  
   64.10  theory Order_Continuity
   64.11  imports Main
    65.1 --- a/src/HOL/Library/Parallel.thy	Sun Nov 02 17:16:01 2014 +0100
    65.2 +++ b/src/HOL/Library/Parallel.thy	Sun Nov 02 17:20:45 2014 +0100
    65.3 @@ -1,6 +1,6 @@
    65.4  (* Author: Florian Haftmann, TU Muenchen *)
    65.5  
    65.6 -header {* Futures and parallel lists for code generated towards Isabelle/ML *}
    65.7 +section {* Futures and parallel lists for code generated towards Isabelle/ML *}
    65.8  
    65.9  theory Parallel
   65.10  imports Main
    66.1 --- a/src/HOL/Library/Permutation.thy	Sun Nov 02 17:16:01 2014 +0100
    66.2 +++ b/src/HOL/Library/Permutation.thy	Sun Nov 02 17:20:45 2014 +0100
    66.3 @@ -2,7 +2,7 @@
    66.4      Author:     Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
    66.5  *)
    66.6  
    66.7 -header {* Permutations *}
    66.8 +section {* Permutations *}
    66.9  
   66.10  theory Permutation
   66.11  imports Multiset
    67.1 --- a/src/HOL/Library/Permutations.thy	Sun Nov 02 17:16:01 2014 +0100
    67.2 +++ b/src/HOL/Library/Permutations.thy	Sun Nov 02 17:20:45 2014 +0100
    67.3 @@ -2,7 +2,7 @@
    67.4      Author:     Amine Chaieb, University of Cambridge
    67.5  *)
    67.6  
    67.7 -header {* Permutations, both general and specifically on finite sets.*}
    67.8 +section {* Permutations, both general and specifically on finite sets.*}
    67.9  
   67.10  theory Permutations
   67.11  imports Fact
    68.1 --- a/src/HOL/Library/Phantom_Type.thy	Sun Nov 02 17:16:01 2014 +0100
    68.2 +++ b/src/HOL/Library/Phantom_Type.thy	Sun Nov 02 17:20:45 2014 +0100
    68.3 @@ -2,7 +2,7 @@
    68.4      Author:     Andreas Lochbihler
    68.5  *)
    68.6  
    68.7 -header {* A generic phantom type *}
    68.8 +section {* A generic phantom type *}
    68.9  
   68.10  theory Phantom_Type
   68.11  imports Main
    69.1 --- a/src/HOL/Library/Poly_Deriv.thy	Sun Nov 02 17:16:01 2014 +0100
    69.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Sun Nov 02 17:20:45 2014 +0100
    69.3 @@ -3,7 +3,7 @@
    69.4      Author:     Brian Huffman
    69.5  *)
    69.6  
    69.7 -header{* Polynomials and Differentiation *}
    69.8 +section{* Polynomials and Differentiation *}
    69.9  
   69.10  theory Poly_Deriv
   69.11  imports Deriv Polynomial
    70.1 --- a/src/HOL/Library/Polynomial.thy	Sun Nov 02 17:16:01 2014 +0100
    70.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Nov 02 17:20:45 2014 +0100
    70.3 @@ -4,7 +4,7 @@
    70.4      Author:     Florian Haftmann
    70.5  *)
    70.6  
    70.7 -header {* Polynomials as type over a ring structure *}
    70.8 +section {* Polynomials as type over a ring structure *}
    70.9  
   70.10  theory Polynomial
   70.11  imports Main GCD "~~/src/HOL/Library/More_List"
    71.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Nov 02 17:16:01 2014 +0100
    71.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Nov 02 17:20:45 2014 +0100
    71.3 @@ -1,6 +1,6 @@
    71.4  (* Author: Lukas Bulwahn, TU Muenchen *)
    71.5  
    71.6 -header {* A Prototype of Quickcheck based on the Predicate Compiler *}
    71.7 +section {* A Prototype of Quickcheck based on the Predicate Compiler *}
    71.8  
    71.9  theory Predicate_Compile_Quickcheck
   71.10  imports Main Predicate_Compile_Alternative_Defs
    72.1 --- a/src/HOL/Library/Prefix_Order.thy	Sun Nov 02 17:16:01 2014 +0100
    72.2 +++ b/src/HOL/Library/Prefix_Order.thy	Sun Nov 02 17:20:45 2014 +0100
    72.3 @@ -2,7 +2,7 @@
    72.4      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
    72.5  *)
    72.6  
    72.7 -header {* Prefix order on lists as order class instance *}
    72.8 +section {* Prefix order on lists as order class instance *}
    72.9  
   72.10  theory Prefix_Order
   72.11  imports Sublist
    73.1 --- a/src/HOL/Library/Preorder.thy	Sun Nov 02 17:16:01 2014 +0100
    73.2 +++ b/src/HOL/Library/Preorder.thy	Sun Nov 02 17:20:45 2014 +0100
    73.3 @@ -1,6 +1,6 @@
    73.4  (* Author: Florian Haftmann, TU Muenchen *)
    73.5  
    73.6 -header {* Preorders with explicit equivalence relation *}
    73.7 +section {* Preorders with explicit equivalence relation *}
    73.8  
    73.9  theory Preorder
   73.10  imports Orderings
    74.1 --- a/src/HOL/Library/Product_Lexorder.thy	Sun Nov 02 17:16:01 2014 +0100
    74.2 +++ b/src/HOL/Library/Product_Lexorder.thy	Sun Nov 02 17:20:45 2014 +0100
    74.3 @@ -2,7 +2,7 @@
    74.4      Author:     Norbert Voelker
    74.5  *)
    74.6  
    74.7 -header {* Lexicographic order on product types *}
    74.8 +section {* Lexicographic order on product types *}
    74.9  
   74.10  theory Product_Lexorder
   74.11  imports Main
    75.1 --- a/src/HOL/Library/Product_Order.thy	Sun Nov 02 17:16:01 2014 +0100
    75.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Nov 02 17:20:45 2014 +0100
    75.3 @@ -2,7 +2,7 @@
    75.4      Author:     Brian Huffman
    75.5  *)
    75.6  
    75.7 -header {* Pointwise order on product types *}
    75.8 +section {* Pointwise order on product types *}
    75.9  
   75.10  theory Product_Order
   75.11  imports Product_plus Conditionally_Complete_Lattices
    76.1 --- a/src/HOL/Library/Product_Vector.thy	Sun Nov 02 17:16:01 2014 +0100
    76.2 +++ b/src/HOL/Library/Product_Vector.thy	Sun Nov 02 17:20:45 2014 +0100
    76.3 @@ -2,7 +2,7 @@
    76.4      Author:     Brian Huffman
    76.5  *)
    76.6  
    76.7 -header {* Cartesian Products as Vector Spaces *}
    76.8 +section {* Cartesian Products as Vector Spaces *}
    76.9  
   76.10  theory Product_Vector
   76.11  imports Inner_Product Product_plus
    77.1 --- a/src/HOL/Library/Product_plus.thy	Sun Nov 02 17:16:01 2014 +0100
    77.2 +++ b/src/HOL/Library/Product_plus.thy	Sun Nov 02 17:20:45 2014 +0100
    77.3 @@ -2,7 +2,7 @@
    77.4      Author:     Brian Huffman
    77.5  *)
    77.6  
    77.7 -header {* Additive group operations on product types *}
    77.8 +section {* Additive group operations on product types *}
    77.9  
   77.10  theory Product_plus
   77.11  imports Main
    78.1 --- a/src/HOL/Library/Quotient_List.thy	Sun Nov 02 17:16:01 2014 +0100
    78.2 +++ b/src/HOL/Library/Quotient_List.thy	Sun Nov 02 17:20:45 2014 +0100
    78.3 @@ -2,7 +2,7 @@
    78.4      Author:     Cezary Kaliszyk and Christian Urban
    78.5  *)
    78.6  
    78.7 -header {* Quotient infrastructure for the list type *}
    78.8 +section {* Quotient infrastructure for the list type *}
    78.9  
   78.10  theory Quotient_List
   78.11  imports Main Quotient_Set Quotient_Product Quotient_Option
    79.1 --- a/src/HOL/Library/Quotient_Option.thy	Sun Nov 02 17:16:01 2014 +0100
    79.2 +++ b/src/HOL/Library/Quotient_Option.thy	Sun Nov 02 17:20:45 2014 +0100
    79.3 @@ -2,7 +2,7 @@
    79.4      Author:     Cezary Kaliszyk and Christian Urban
    79.5  *)
    79.6  
    79.7 -header {* Quotient infrastructure for the option type *}
    79.8 +section {* Quotient infrastructure for the option type *}
    79.9  
   79.10  theory Quotient_Option
   79.11  imports Main Quotient_Syntax
    80.1 --- a/src/HOL/Library/Quotient_Product.thy	Sun Nov 02 17:16:01 2014 +0100
    80.2 +++ b/src/HOL/Library/Quotient_Product.thy	Sun Nov 02 17:20:45 2014 +0100
    80.3 @@ -2,7 +2,7 @@
    80.4      Author:     Cezary Kaliszyk and Christian Urban
    80.5  *)
    80.6  
    80.7 -header {* Quotient infrastructure for the product type *}
    80.8 +section {* Quotient infrastructure for the product type *}
    80.9  
   80.10  theory Quotient_Product
   80.11  imports Main Quotient_Syntax
    81.1 --- a/src/HOL/Library/Quotient_Set.thy	Sun Nov 02 17:16:01 2014 +0100
    81.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sun Nov 02 17:20:45 2014 +0100
    81.3 @@ -2,7 +2,7 @@
    81.4      Author:     Cezary Kaliszyk and Christian Urban
    81.5  *)
    81.6  
    81.7 -header {* Quotient infrastructure for the set type *}
    81.8 +section {* Quotient infrastructure for the set type *}
    81.9  
   81.10  theory Quotient_Set
   81.11  imports Main Quotient_Syntax
    82.1 --- a/src/HOL/Library/Quotient_Sum.thy	Sun Nov 02 17:16:01 2014 +0100
    82.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Sun Nov 02 17:20:45 2014 +0100
    82.3 @@ -2,7 +2,7 @@
    82.4      Author:     Cezary Kaliszyk and Christian Urban
    82.5  *)
    82.6  
    82.7 -header {* Quotient infrastructure for the sum type *}
    82.8 +section {* Quotient infrastructure for the sum type *}
    82.9  
   82.10  theory Quotient_Sum
   82.11  imports Main Quotient_Syntax
    83.1 --- a/src/HOL/Library/Quotient_Syntax.thy	Sun Nov 02 17:16:01 2014 +0100
    83.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Sun Nov 02 17:20:45 2014 +0100
    83.3 @@ -2,7 +2,7 @@
    83.4      Author:     Cezary Kaliszyk and Christian Urban
    83.5  *)
    83.6  
    83.7 -header {* Pretty syntax for Quotient operations *}
    83.8 +section {* Pretty syntax for Quotient operations *}
    83.9  
   83.10  theory Quotient_Syntax
   83.11  imports Main
    84.1 --- a/src/HOL/Library/Quotient_Type.thy	Sun Nov 02 17:16:01 2014 +0100
    84.2 +++ b/src/HOL/Library/Quotient_Type.thy	Sun Nov 02 17:20:45 2014 +0100
    84.3 @@ -2,7 +2,7 @@
    84.4      Author:     Markus Wenzel, TU Muenchen
    84.5  *)
    84.6  
    84.7 -header {* Quotient types *}
    84.8 +section {* Quotient types *}
    84.9  
   84.10  theory Quotient_Type
   84.11  imports Main
    85.1 --- a/src/HOL/Library/RBT.thy	Sun Nov 02 17:16:01 2014 +0100
    85.2 +++ b/src/HOL/Library/RBT.thy	Sun Nov 02 17:20:45 2014 +0100
    85.3 @@ -2,7 +2,7 @@
    85.4      Author:     Lukas Bulwahn and Ondrej Kuncar
    85.5  *)
    85.6  
    85.7 -header {* Abstract type of RBT trees *}
    85.8 +section {* Abstract type of RBT trees *}
    85.9  
   85.10  theory RBT 
   85.11  imports Main RBT_Impl
    86.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Nov 02 17:16:01 2014 +0100
    86.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Nov 02 17:20:45 2014 +0100
    86.3 @@ -3,7 +3,7 @@
    86.4      Author:     Alexander Krauss, TU Muenchen
    86.5  *)
    86.6  
    86.7 -header {* Implementation of Red-Black Trees *}
    86.8 +section {* Implementation of Red-Black Trees *}
    86.9  
   86.10  theory RBT_Impl
   86.11  imports Main
    87.1 --- a/src/HOL/Library/RBT_Mapping.thy	Sun Nov 02 17:16:01 2014 +0100
    87.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Sun Nov 02 17:20:45 2014 +0100
    87.3 @@ -2,7 +2,7 @@
    87.4      Author:     Florian Haftmann and Ondrej Kuncar
    87.5  *)
    87.6  
    87.7 -header {* Implementation of mappings with Red-Black Trees *}
    87.8 +section {* Implementation of mappings with Red-Black Trees *}
    87.9  
   87.10  (*<*)
   87.11  theory RBT_Mapping
    88.1 --- a/src/HOL/Library/RBT_Set.thy	Sun Nov 02 17:16:01 2014 +0100
    88.2 +++ b/src/HOL/Library/RBT_Set.thy	Sun Nov 02 17:20:45 2014 +0100
    88.3 @@ -2,7 +2,7 @@
    88.4      Author:     Ondrej Kuncar
    88.5  *)
    88.6  
    88.7 -header {* Implementation of sets using RBT trees *}
    88.8 +section {* Implementation of sets using RBT trees *}
    88.9  
   88.10  theory RBT_Set
   88.11  imports RBT Product_Lexorder
    89.1 --- a/src/HOL/Library/Ramsey.thy	Sun Nov 02 17:16:01 2014 +0100
    89.2 +++ b/src/HOL/Library/Ramsey.thy	Sun Nov 02 17:20:45 2014 +0100
    89.3 @@ -2,7 +2,7 @@
    89.4      Author:     Tom Ridge.  Converted to structured Isar by L C Paulson
    89.5  *)
    89.6  
    89.7 -header "Ramsey's Theorem"
    89.8 +section "Ramsey's Theorem"
    89.9  
   89.10  theory Ramsey
   89.11  imports Main Infinite_Set
    90.1 --- a/src/HOL/Library/Reflection.thy	Sun Nov 02 17:16:01 2014 +0100
    90.2 +++ b/src/HOL/Library/Reflection.thy	Sun Nov 02 17:20:45 2014 +0100
    90.3 @@ -2,7 +2,7 @@
    90.4      Author:     Amine Chaieb, TU Muenchen
    90.5  *)
    90.6  
    90.7 -header {* Generic reflection and reification *}
    90.8 +section {* Generic reflection and reification *}
    90.9  
   90.10  theory Reflection
   90.11  imports Main
    91.1 --- a/src/HOL/Library/Refute.thy	Sun Nov 02 17:16:01 2014 +0100
    91.2 +++ b/src/HOL/Library/Refute.thy	Sun Nov 02 17:20:45 2014 +0100
    91.3 @@ -5,7 +5,7 @@
    91.4  Basic setup and documentation for the 'refute' (and 'refute_params') command.
    91.5  *)
    91.6  
    91.7 -header {* Refute *}
    91.8 +section {* Refute *}
    91.9  
   91.10  theory Refute
   91.11  imports Main
    92.1 --- a/src/HOL/Library/Saturated.thy	Sun Nov 02 17:16:01 2014 +0100
    92.2 +++ b/src/HOL/Library/Saturated.thy	Sun Nov 02 17:20:45 2014 +0100
    92.3 @@ -4,7 +4,7 @@
    92.4      Author:     Florian Haftmann
    92.5  *)
    92.6  
    92.7 -header {* Saturated arithmetic *}
    92.8 +section {* Saturated arithmetic *}
    92.9  
   92.10  theory Saturated
   92.11  imports Numeral_Type "~~/src/HOL/Word/Type_Length"
    93.1 --- a/src/HOL/Library/Set_Algebras.thy	Sun Nov 02 17:16:01 2014 +0100
    93.2 +++ b/src/HOL/Library/Set_Algebras.thy	Sun Nov 02 17:20:45 2014 +0100
    93.3 @@ -2,7 +2,7 @@
    93.4      Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
    93.5  *)
    93.6  
    93.7 -header {* Algebraic operations on sets *}
    93.8 +section {* Algebraic operations on sets *}
    93.9  
   93.10  theory Set_Algebras
   93.11  imports Main
    94.1 --- a/src/HOL/Library/State_Monad.thy	Sun Nov 02 17:16:01 2014 +0100
    94.2 +++ b/src/HOL/Library/State_Monad.thy	Sun Nov 02 17:20:45 2014 +0100
    94.3 @@ -2,7 +2,7 @@
    94.4      Author:     Florian Haftmann, TU Muenchen
    94.5  *)
    94.6  
    94.7 -header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
    94.8 +section {* Combinator syntax for generic, open state monads (single-threaded monads) *}
    94.9  
   94.10  theory State_Monad
   94.11  imports Main Monad_Syntax
    95.1 --- a/src/HOL/Library/Stream.thy	Sun Nov 02 17:16:01 2014 +0100
    95.2 +++ b/src/HOL/Library/Stream.thy	Sun Nov 02 17:20:45 2014 +0100
    95.3 @@ -6,7 +6,7 @@
    95.4  Infinite streams.
    95.5  *)
    95.6  
    95.7 -header {* Infinite Streams *}
    95.8 +section {* Infinite Streams *}
    95.9  
   95.10  theory Stream
   95.11  imports "~~/src/HOL/Library/Nat_Bijection"
    96.1 --- a/src/HOL/Library/Sublist.thy	Sun Nov 02 17:16:01 2014 +0100
    96.2 +++ b/src/HOL/Library/Sublist.thy	Sun Nov 02 17:20:45 2014 +0100
    96.3 @@ -3,7 +3,7 @@
    96.4      Author:     Christian Sternagel, JAIST
    96.5  *)
    96.6  
    96.7 -header {* List prefixes, suffixes, and homeomorphic embedding *}
    96.8 +section {* List prefixes, suffixes, and homeomorphic embedding *}
    96.9  
   96.10  theory Sublist
   96.11  imports Main
    97.1 --- a/src/HOL/Library/Sublist_Order.thy	Sun Nov 02 17:16:01 2014 +0100
    97.2 +++ b/src/HOL/Library/Sublist_Order.thy	Sun Nov 02 17:20:45 2014 +0100
    97.3 @@ -3,7 +3,7 @@
    97.4                  Florian Haftmann, Tobias Nipkow, TU Muenchen
    97.5  *)
    97.6  
    97.7 -header {* Sublist Ordering *}
    97.8 +section {* Sublist Ordering *}
    97.9  
   97.10  theory Sublist_Order
   97.11  imports Sublist
    98.1 --- a/src/HOL/Library/Sum_of_Squares.thy	Sun Nov 02 17:16:01 2014 +0100
    98.2 +++ b/src/HOL/Library/Sum_of_Squares.thy	Sun Nov 02 17:20:45 2014 +0100
    98.3 @@ -3,7 +3,7 @@
    98.4      Author:     Philipp Meyer, TU Muenchen
    98.5  *)
    98.6  
    98.7 -header {* A decision procedure for universal multivariate real arithmetic
    98.8 +section {* A decision procedure for universal multivariate real arithmetic
    98.9    with addition, multiplication and ordering using semidefinite programming *}
   98.10  
   98.11  theory Sum_of_Squares
    99.1 --- a/src/HOL/Library/Sum_of_Squares_Remote.thy	Sun Nov 02 17:16:01 2014 +0100
    99.2 +++ b/src/HOL/Library/Sum_of_Squares_Remote.thy	Sun Nov 02 17:20:45 2014 +0100
    99.3 @@ -3,7 +3,7 @@
    99.4      Author:     Philipp Meyer, TU Muenchen
    99.5  *)
    99.6  
    99.7 -header {* Examples with remote CSDP *}
    99.8 +section {* Examples with remote CSDP *}
    99.9  
   99.10  theory Sum_of_Squares_Remote
   99.11  imports Sum_of_Squares
   100.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Sun Nov 02 17:16:01 2014 +0100
   100.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Sun Nov 02 17:20:45 2014 +0100
   100.3 @@ -1,6 +1,6 @@
   100.4  (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
   100.5  
   100.6 -header {* A table-based implementation of the reflexive transitive closure *}
   100.7 +section {* A table-based implementation of the reflexive transitive closure *}
   100.8  
   100.9  theory Transitive_Closure_Table
  100.10  imports Main
   101.1 --- a/src/HOL/Library/Tree.thy	Sun Nov 02 17:16:01 2014 +0100
   101.2 +++ b/src/HOL/Library/Tree.thy	Sun Nov 02 17:20:45 2014 +0100
   101.3 @@ -1,6 +1,6 @@
   101.4  (* Author: Tobias Nipkow *)
   101.5  
   101.6 -header {* Binary Tree *}
   101.7 +section {* Binary Tree *}
   101.8  
   101.9  theory Tree
  101.10  imports Main
   102.1 --- a/src/HOL/Library/While_Combinator.thy	Sun Nov 02 17:16:01 2014 +0100
   102.2 +++ b/src/HOL/Library/While_Combinator.thy	Sun Nov 02 17:20:45 2014 +0100
   102.3 @@ -3,7 +3,7 @@
   102.4      Author:     Alexander Krauss
   102.5  *)
   102.6  
   102.7 -header {* A general ``while'' combinator *}
   102.8 +section {* A general ``while'' combinator *}
   102.9  
  102.10  theory While_Combinator
  102.11  imports Main
   103.1 --- a/src/HOL/Library/document/root.tex	Sun Nov 02 17:16:01 2014 +0100
   103.2 +++ b/src/HOL/Library/document/root.tex	Sun Nov 02 17:20:45 2014 +0100
   103.3 @@ -18,9 +18,7 @@
   103.4  \tableofcontents
   103.5  \newpage
   103.6  
   103.7 -\renewcommand{\isamarkupheader}[1]%
   103.8 -{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
   103.9 -\markright{THEORY~``\isabellecontext''}}
  103.10 +\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
  103.11  
  103.12  \input{session}
  103.13