# HG changeset patch # User wenzelm # Date 1414948905 -3600 # Node ID 5b7a9633cfa83d5ab16bb5ce4a89c81406cca513 # Parent 9537bf1c4853652c633378748fd929711abd62f8 modernized header uniformly as section; diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/CCL.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Fix.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Gfp.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Hered.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Lfp.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Set.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Term.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Trancl.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Type.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/Wfd.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/ex/Flag.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/ex/List.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/ex/Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CCL/ex/Stream.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/Arith.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/Bool.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/CTT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/Main.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/ex/Elimination.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/ex/Equality.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/ex/Synthesis.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/CTT/ex/Typechecking.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Cube/Cube.thy --- 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 \Barendregt's Lambda-Cube\ +section \Barendregt's Lambda-Cube\ theory Cube imports Pure diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Cube/Example.thy --- 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 \Lambda Cube Examples\ +section \Lambda Cube Examples\ theory Example imports Cube diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Isar_Ref/First_Order_Logic.thy --- 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 \Example: First-Order Logic\ +section \Example: First-Order Logic\ theory %visible First_Order_Logic imports Base (* FIXME Pure!? *) diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Logics_ZF/FOL_examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Logics_ZF/IFOL_examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Logics_ZF/ZF_examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Tutorial/Protocol/Event.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Tutorial/Protocol/Message.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Doc/Tutorial/Types/Records.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/FOL.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/IFOL.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Classical.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/First_Order_Logic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Foundation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/If.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Intro.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Intuitionistic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Natural_Numbers.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Prolog.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Propositional_Cla.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Propositional_Int.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Quantifiers_Cla.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOL/ex/Quantifiers_Int.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/FOLP.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/IFOLP.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/ex/Foundation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/ex/Intro.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/ex/Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/ex/Propositional_Cla.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/FOLP/ex/Propositional_Int.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ATP.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Algebra/Divisibility.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Archimedean_Field.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Auth_Public.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Auth_Shared.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/CertifiedEmail.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Event.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Analz.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Auth_Guard_Public.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Auth_Guard_Shared.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Extensions.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Guard.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/GuardK.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Guard_NS_Public.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Guard_OtwayRees.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Guard_Shared.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Guard_Yahalom.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/List_Msg.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/P1.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/P2.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Guard/Proto.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/KerberosIV.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/KerberosIV_Gets.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/KerberosV.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Kerberos_BAN.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Kerberos_BAN_Gets.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Message.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/NS_Public.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/NS_Public_Bad.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/NS_Shared.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/OtwayRees.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/OtwayReesBella.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/OtwayRees_AN.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/OtwayRees_Bad.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Recur.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Smartcard/Auth_Smartcard.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Smartcard/EventSC.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Smartcard/ShoupRubin.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Smartcard/Smartcard.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/TLS.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/WooLam.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Yahalom.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Yahalom2.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Auth/Yahalom_Bad.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Cardinal_Arithmetic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Cardinal_Order_Relation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Composition.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Def.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Fixpoint_Base.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Greatest_Fixpoint.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Least_Fixpoint.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Wellorder_Constructions.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Wellorder_Embedding.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/BNF_Wellorder_Relation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Basic_BNFs.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Cardinal_Arithmetic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Cardinal_Order_Relation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Cardinals.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Fun_More.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Order_Relation_More.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Order_Union.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Ordinal_Arithmetic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Wellfounded_More.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Wellorder_Constructions.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Wellorder_Embedding.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Wellorder_Extension.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Cardinals/Wellorder_Relation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Code_Evaluation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Code_Numeral.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Codegenerator_Test/Candidates.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Codegenerator_Test/Generate.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Codegenerator_Test/Generate_Target_Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Coinduction.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Complete_Lattices.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Complete_Partial_Order.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Complex.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Complex_Main.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Conditionally_Complete_Lattices.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Ctr_Sugar.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Compat.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Derivation_Trees/DTree.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Derivation_Trees/Parallel.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/IsaFoR.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Koenig.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Lambda_Term.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Misc_Codatatype.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Misc_Datatype.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Misc_N2M.thy --- 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 \Miscellaneous Tests for the Nested-to-Mutual Reduction\ +section \Miscellaneous Tests for the Nested-to-Mutual Reduction\ theory Misc_N2M imports "~~/src/HOL/Library/BNF_Axiomatization" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Misc_Primcorec.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Misc_Primrec.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Process.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/Stream_Processor.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/TreeFI.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Datatype_Examples/TreeFsetI.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Approximation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Commutative_Ring.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Polynomial_List.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Rat_Pair.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Deriv.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Divides.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Enum.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Equiv_Relations.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Extraction.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Fact.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Fields.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Finite_Set.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Fun.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Fun_Def.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Fun_Def_Base.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/GCD.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Groebner_Basis.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Groups.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Groups_Big.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Groups_List.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/HOL.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Bounds.thy --- 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 \Bounds\ +section \Bounds\ theory Bounds imports Main "~~/src/HOL/Library/ContNotDenum" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Function_Norm.thy --- 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 \The norm of a function\ +section \The norm of a function\ theory Function_Norm imports Normed_Space Function_Order diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Function_Order.thy --- 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 \An order on functions\ +section \An order on functions\ theory Function_Order imports Subspace Linearform diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Hahn_Banach.thy --- 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 \The Hahn-Banach Theorem\ +section \The Hahn-Banach Theorem\ theory Hahn_Banach imports Hahn_Banach_Lemmas diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy --- 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 \Extending non-maximal functions\ +section \Extending non-maximal functions\ theory Hahn_Banach_Ext_Lemmas imports Function_Norm diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy --- 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 \The supremum w.r.t.~the function order\ +section \The supremum w.r.t.~the function order\ theory Hahn_Banach_Sup_Lemmas imports Function_Norm Zorn_Lemma diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Linearform.thy --- 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 \Linearforms\ +section \Linearforms\ theory Linearform imports Vector_Space diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Normed_Space.thy --- 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 \Normed vector spaces\ +section \Normed vector spaces\ theory Normed_Space imports Subspace diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Subspace.thy --- 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 \Subspaces\ +section \Subspaces\ theory Subspace imports Vector_Space "~~/src/HOL/Library/Set_Algebras" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Vector_Space.thy --- 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 \Vector spaces\ +section \Vector spaces\ theory Vector_Space imports Complex_Main Bounds diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hahn_Banach/Zorn_Lemma.thy --- 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 \Zorn's Lemma\ +section \Zorn's Lemma\ theory Zorn_Lemma imports Main diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Hilbert_Choice.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/AExp.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/ASM.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Com.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Compiler.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Complete_Lattice.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Denotational.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Hoare.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Live.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Procs.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Sec_Type_Expr.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Sem_Equiv.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Small_Step.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Types.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMP/Vars.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMPP/Com.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMPP/EvenOdd.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMPP/Hoare.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMPP/Misc.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IMPP/Natural.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IOA/Asig.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IOA/IOA.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/IOA/Solve.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/Array.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/Heap.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/Imperative_HOL.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/Ref.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/SatChecker.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/Sorted_List.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/Subarray.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Imperative_HOL/ex/Sublist.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Import/HOL_Light_Import.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Import/HOL_Light_Maps.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Import/Import_Setup.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/ABexp.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Com.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Comb.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Common_Patterns.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Ordinals.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/PropLog.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/QuoDataType.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/QuoNestedDataType.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/SList.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Sigma_Algebra.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Term.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Induct/Tree.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Inductive.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Int.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lattices.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lattices_Big.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lazy_Sequence.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lifting.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lifting_Option.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lifting_Product.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lifting_Set.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Lifting_Sum.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Limited_Sequence.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Limits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/List.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/MacLaurin.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Main.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Map.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Matrix_LP/ComputeFloat.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Meson.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Abstraction.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Big_O.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Binary_Tree.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Clausification.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Message.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Proxies.thy --- 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. *} diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Sets.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Tarski.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Trans_Closure.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Metis_Examples/Type_Encodings.thy --- 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 *} diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Mirabelle/Mirabelle_Test.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/AxSem.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/Decl.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/Equivalence.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/Example.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/OpSem.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/State.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/Term.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NanoJava/TypeRel.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nat_Transfer.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Core_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Hotel_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Induct_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Integer_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Mini_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Pattern_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Record_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Special_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Tests_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nominal/Examples/Nominal_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nominal/Examples/Nominal_Examples_Base.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nominal/Examples/Pattern.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Nominal/Examples/Standardization.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/NthRoot.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Num.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Binomial.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Cong.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Eratosthenes.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Fib.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Gauss.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Number_Theory.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Pocklington.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Primes.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/Residues.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Number_Theory/UniqueFactorization.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Numeral_Simprocs.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/BijectionRel.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Chinese.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Euler.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/EulerFermat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/EvenOdd.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Factorization.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Fib.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Finite2.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Gauss.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Int2.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/IntFact.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/IntPrimes.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Legacy_GCD.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Pocklington.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Primes.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/Residues.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/WilsonBij.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Old_Number_Theory/WilsonRuss.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Option.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Order_Relation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Orderings.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Parity.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Partial_Function.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Power.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Predicate.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Predicate_Compile.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Presburger.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Product_Type.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Prolog/Func.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Prolog/HOHH.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Prolog/Test.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Prolog/Type.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/Euclid.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/Higman.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/Pigeonhole.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/QuotRem.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/Util.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Extraction/Warshall.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/Commutation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/Eta.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/InductTermi.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/Lambda.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/LambdaType.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/ListApplication.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/ListBeta.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/ListOrder.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/NormalForm.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/ParRed.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/Standardization.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/StrongNorm.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/Lambda/WeakNorm.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Proofs/ex/Hilbert_Classical.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quickcheck_Examples/Completeness.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quickcheck_Exhaustive.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quickcheck_Narrowing.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quickcheck_Random.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quotient.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quotient_Examples/DList.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quotient_Examples/Lift_FSet.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quotient_Examples/Lift_Fun.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Quotient_Examples/Lift_Set.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Random.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Random_Pred.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Random_Sequence.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Rat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Real.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Real_Vector_Spaces.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Record.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Record_Benchmark/Record_Benchmark.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Relation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Rings.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SAT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SET_Protocol/Cardholder_Registration.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SET_Protocol/Event_SET.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SET_Protocol/Merchant_Registration.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SET_Protocol/Message_SET.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SET_Protocol/Public_SET.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SET_Protocol/Purchase.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SMT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SMT_Examples/Boogie.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SMT_Examples/SMT_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SMT_Examples/SMT_Tests.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/SMT_Examples/SMT_Word_Examples.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Semiring_Normalization.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Series.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Set.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Set_Interval.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Sledgehammer.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Statespace/DistinctTreeProver.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Statespace/StateFun.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Statespace/StateSpaceEx.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Statespace/StateSpaceLocale.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Statespace/StateSpaceSyntax.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/String.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Sum_Type.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Action.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Buffer/Buffer.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Buffer/DBuffer.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Inc/Inc.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Intensional.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/MemClerk.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/MemClerkParameters.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/Memory.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/MemoryImplementation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/MemoryParameters.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/ProcedureInterface.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/RPC.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/RPCMemoryParams.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Memory/RPCParameters.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/Stfun.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TLA/TLA.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TPTP/ATP_Problem_Import.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TPTP/ATP_Theory_Export.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TPTP/MaSh_Eval.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TPTP/MaSh_Export.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/TPTP/MaSh_Export_Base.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Taylor.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Topological_Spaces.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Transcendental.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Transfer.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Transitive_Closure.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Typedef.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Typerep.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/AllocBase.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/AllocImpl.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/Client.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/Counter.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/Counterc.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/Priority.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Comp/Progress.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Constrains.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Detects.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/ELT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Extend.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/FP.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Follows.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Guar.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Lift_prog.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/ListOrder.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/ProgressSets.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Project.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Rename.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Simple/NSP_Bad.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Simple/Token.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/SubstAx.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Transformers.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/UNITY.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/UNITY_Main.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/Union.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/UNITY/WFair.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Unix/Nested_Environment.thy --- 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 \Nested environments\ +section \Nested environments\ theory Nested_Environment imports Main diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Unix/Unix.thy --- 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 \Unix file-systems \label{sec:unix-file-system}\ +section \Unix file-systems \label{sec:unix-file-system}\ theory Unix imports diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Wellfounded.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Wfrec.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/Zorn.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Abstract_NAT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Adhoc_Overloading_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Antiquote.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Arith_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/BT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/BinEx.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Birthday_Paradox.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Bubblesort.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/CTL.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Cartouche_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Case_Product.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Chinese.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Classical.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Code_Binary_Nat_examples.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Coherent.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Eval_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Execute_Choice.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/FinFunPred.thy --- 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 *} diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Fundefs.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Gauge_Integration.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Groebner_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Guess.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/HarmonicSeries.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Hebrew.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Hex_Bin_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Higher_Order_Logic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Iff_Oracle.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Induction_Schema.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Intuitionistic.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Lagrange.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/List_to_Set_Comprehension_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/LocaleTest2.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/ML.thy --- 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 \Isabelle/ML basics\ +section \Isabelle/ML basics\ theory "ML" imports Main diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/MT.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/MergeSort.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Meson_Test.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/MonoidGroup.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Multiquote.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/NatSum.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Normalization_by_Evaluation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/PER.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Parallel_Example.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/PresburgerEx.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Primrec.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Quicksort.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Records.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Reflection_Examples.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Refute_Examples.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/SAT_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/SVC_Oracle.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Seq.thy --- 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 \Finite sequences\ +section \Finite sequences\ theory Seq imports Main diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Serbian.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Set_Theory.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Simproc_Tests.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Sqrt.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Sqrt_Script.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Sudoku.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Tarski.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Termination.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/ThreeDivides.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Transfer_Ex.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Transfer_Int_Nat.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Transitive_Closure_Table_Ex.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Tree23.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/Unification.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/While_Combinator_Example.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/HOL/ex/svc_test.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/LCF/LCF.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/LCF/ex/Ex1.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/LCF/ex/Ex2.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/LCF/ex/Ex3.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/LCF/ex/Ex4.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Sequents/LK/Nat.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Sequents/LK/Propositional.thy --- 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" diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Sequents/LK0.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Sequents/Sequents.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Tools/Adhoc_Overloading.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Tools/Code_Generator.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Tools/Permanent_Interpretation.thy --- 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 diff -r 9537bf1c4853 -r 5b7a9633cfa8 src/Tools/SML/Examples.thy --- 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 \Standard ML within the Isabelle environment\ +section \Standard ML within the Isabelle environment\ theory Examples imports Pure