--- a/src/ZF/AC.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/AC.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*The Axiom of Choice*}
+section{*The Axiom of Choice*}
theory AC imports Main_ZF begin
--- a/src/ZF/Arith.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Arith.thy Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
Also, rec(m, 0, %z w.z) is pred(m).
*)
-header{*Arithmetic Operators and Their Definitions*}
+section{*Arithmetic Operators and Their Definitions*}
theory Arith imports Univ begin
--- a/src/ZF/ArithSimp.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ArithSimp.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 University of Cambridge
*)
-header{*Arithmetic with simplification*}
+section{*Arithmetic with simplification*}
theory ArithSimp
imports Arith
--- a/src/ZF/Bin.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Bin.thy Sun Nov 02 16:39:54 2014 +0100
@@ -13,7 +13,7 @@
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
*)
-header{*Arithmetic on Binary Integers*}
+section{*Arithmetic on Binary Integers*}
theory Bin
imports Int_ZF Datatype_ZF
--- a/src/ZF/Bool.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Bool.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1992 University of Cambridge
*)
-header{*Booleans in Zermelo-Fraenkel Set Theory*}
+section{*Booleans in Zermelo-Fraenkel Set Theory*}
theory Bool imports pair begin
--- a/src/ZF/Cardinal.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Cardinal.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Cardinal Numbers Without the Axiom of Choice*}
+section{*Cardinal Numbers Without the Axiom of Choice*}
theory Cardinal imports OrderType Finite Nat_ZF Sum begin
--- a/src/ZF/CardinalArith.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/CardinalArith.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Cardinal Arithmetic Without the Axiom of Choice*}
+section{*Cardinal Arithmetic Without the Axiom of Choice*}
theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begin
--- a/src/ZF/Cardinal_AC.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Cardinal_AC.thy Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
These results help justify infinite-branching datatypes
*)
-header{*Cardinal Arithmetic Using AC*}
+section{*Cardinal Arithmetic Using AC*}
theory Cardinal_AC imports CardinalArith Zorn begin
--- a/src/ZF/Constructible/AC_in_L.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {* The Axiom of Choice Holds in L! *}
+section {* The Axiom of Choice Holds in L! *}
theory AC_in_L imports Formula Separation begin
--- a/src/ZF/Constructible/DPow_absolute.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Absoluteness for the Definable Powerset Function*}
+section {*Absoluteness for the Definable Powerset Function*}
theory DPow_absolute imports Satisfies_absolute begin
--- a/src/ZF/Constructible/Datatype_absolute.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Absoluteness Properties for Recursive Datatypes*}
+section {*Absoluteness Properties for Recursive Datatypes*}
theory Datatype_absolute imports Formula WF_absolute begin
--- a/src/ZF/Constructible/Formula.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Formula.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {* First-Order Formulas and the Definition of the Class L *}
+section {* First-Order Formulas and the Definition of the Class L *}
theory Formula imports Main begin
--- a/src/ZF/Constructible/L_axioms.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {* The ZF Axioms (Except Separation) in L *}
+section {* The ZF Axioms (Except Separation) in L *}
theory L_axioms imports Formula Relative Reflection MetaExists begin
--- a/src/ZF/Constructible/MetaExists.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/MetaExists.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header{*The meta-existential quantifier*}
+section{*The meta-existential quantifier*}
theory MetaExists imports Main begin
--- a/src/ZF/Constructible/Normal.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Normal.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Closed Unbounded Classes and Normal Functions*}
+section {*Closed Unbounded Classes and Normal Functions*}
theory Normal imports Main begin
--- a/src/ZF/Constructible/Rank.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Rank.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Absoluteness for Order Types, Rank Functions and Well-Founded
+section {*Absoluteness for Order Types, Rank Functions and Well-Founded
Relations*}
theory Rank imports WF_absolute begin
--- a/src/ZF/Constructible/Rank_Separation.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Separation for Facts About Order Types, Rank Functions and
+section {*Separation for Facts About Order Types, Rank Functions and
Well-Founded Relations*}
theory Rank_Separation imports Rank Rec_Separation begin
--- a/src/ZF/Constructible/Rec_Separation.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Separation for Facts About Recursion*}
+section {*Separation for Facts About Recursion*}
theory Rec_Separation imports Separation Internalize begin
--- a/src/ZF/Constructible/Reflection.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Reflection.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {* The Reflection Theorem*}
+section {* The Reflection Theorem*}
theory Reflection imports Normal begin
--- a/src/ZF/Constructible/Relative.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Relative.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Relativization and Absoluteness*}
+section {*Relativization and Absoluteness*}
theory Relative imports Main begin
--- a/src/ZF/Constructible/Satisfies_absolute.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Absoluteness for the Satisfies Relation on Formulas*}
+section {*Absoluteness for the Satisfies Relation on Formulas*}
theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin
--- a/src/ZF/Constructible/Separation.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Separation.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header{*Early Instances of Separation and Strong Replacement*}
+section{*Early Instances of Separation and Strong Replacement*}
theory Separation imports L_axioms WF_absolute begin
--- a/src/ZF/Constructible/WF_absolute.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/WF_absolute.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Absoluteness of Well-Founded Recursion*}
+section {*Absoluteness of Well-Founded Recursion*}
theory WF_absolute imports WFrec begin
--- a/src/ZF/Constructible/WFrec.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/WFrec.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header{*Relativized Well-Founded Recursion*}
+section{*Relativized Well-Founded Recursion*}
theory WFrec imports Wellorderings begin
--- a/src/ZF/Constructible/Wellorderings.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Relativized Wellorderings*}
+section {*Relativized Wellorderings*}
theory Wellorderings imports Relative begin
--- a/src/ZF/Datatype_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Datatype_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1997 University of Cambridge
*)
-header{*Datatype and CoDatatype Definitions*}
+section{*Datatype and CoDatatype Definitions*}
theory Datatype_ZF
imports Inductive_ZF Univ QUniv
--- a/src/ZF/Epsilon.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Epsilon.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
*)
-header{*Epsilon Induction and Recursion*}
+section{*Epsilon Induction and Recursion*}
theory Epsilon imports Nat_ZF begin
--- a/src/ZF/EquivClass.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/EquivClass.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Equivalence Relations*}
+section{*Equivalence Relations*}
theory EquivClass imports Trancl Perm begin
--- a/src/ZF/Finite.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Finite.thy Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
prove: b \<in> Fin(A) ==> inj(b,b) \<subseteq> surj(b,b)
*)
-header{*Finite Powerset Operator and Finite Function Space*}
+section{*Finite Powerset Operator and Finite Function Space*}
theory Finite imports Inductive_ZF Epsilon Nat_ZF begin
--- a/src/ZF/Fixedpt.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Fixedpt.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1992 University of Cambridge
*)
-header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
+section{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
theory Fixedpt imports equalities begin
--- a/src/ZF/IMP/Com.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IMP/Com.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
-header {* Arithmetic expressions, boolean expressions, commands *}
+section {* Arithmetic expressions, boolean expressions, commands *}
theory Com imports Main begin
--- a/src/ZF/IMP/Denotation.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IMP/Denotation.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
-header {* Denotational semantics of expressions and commands *}
+section {* Denotational semantics of expressions and commands *}
theory Denotation imports Com begin
--- a/src/ZF/IMP/Equiv.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IMP/Equiv.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
-header {* Equivalence *}
+section {* Equivalence *}
theory Equiv imports Denotation Com begin
--- a/src/ZF/Induct/Acc.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Acc.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* The accessible part of a relation *}
+section {* The accessible part of a relation *}
theory Acc imports Main begin
--- a/src/ZF/Induct/Binary_Trees.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1992 University of Cambridge
*)
-header {* Binary trees *}
+section {* Binary trees *}
theory Binary_Trees imports Main begin
--- a/src/ZF/Induct/Brouwer.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Brouwer.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Infinite branching datatype definitions *}
+section {* Infinite branching datatype definitions *}
theory Brouwer imports Main_ZFC begin
--- a/src/ZF/Induct/Comb.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Comb.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Combinatory Logic example: the Church-Rosser Theorem *}
+section {* Combinatory Logic example: the Church-Rosser Theorem *}
theory Comb imports Main begin
--- a/src/ZF/Induct/Datatypes.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Datatypes.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Sample datatype definitions *}
+section {* Sample datatype definitions *}
theory Datatypes imports Main begin
--- a/src/ZF/Induct/ListN.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/ListN.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Lists of n elements *}
+section {* Lists of n elements *}
theory ListN imports Main begin
--- a/src/ZF/Induct/Mutil.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Mutil.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1996 University of Cambridge
*)
-header {* The Mutilated Chess Board Problem, formalized inductively *}
+section {* The Mutilated Chess Board Problem, formalized inductively *}
theory Mutil imports Main begin
--- a/src/ZF/Induct/Ntree.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Ntree.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Datatype definition n-ary branching trees *}
+section {* Datatype definition n-ary branching trees *}
theory Ntree imports Main begin
--- a/src/ZF/Induct/Primrec.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Primrec.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Primitive Recursive Functions: the inductive definition *}
+section {* Primitive Recursive Functions: the inductive definition *}
theory Primrec imports Main begin
--- a/src/ZF/Induct/PropLog.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/PropLog.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
*)
-header {* Meta-theory of propositional logic *}
+section {* Meta-theory of propositional logic *}
theory PropLog imports Main begin
--- a/src/ZF/Induct/Rmap.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Rmap.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* An operator to ``map'' a relation over a list *}
+section {* An operator to ``map'' a relation over a list *}
theory Rmap imports Main begin
--- a/src/ZF/Induct/Term.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Term.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Terms over an alphabet *}
+section {* Terms over an alphabet *}
theory Term imports Main begin
--- a/src/ZF/Induct/Tree_Forest.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Trees and forests, a mutually recursive type definition *}
+section {* Trees and forests, a mutually recursive type definition *}
theory Tree_Forest imports Main begin
--- a/src/ZF/Inductive_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
Products are used only to derive "streamlined" induction rules for relations
*)
-header{*Inductive and Coinductive Definitions*}
+section{*Inductive and Coinductive Definitions*}
theory Inductive_ZF
imports Fixedpt QPair Nat_ZF
--- a/src/ZF/InfDatatype.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/InfDatatype.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Infinite-Branching Datatype Definitions*}
+section{*Infinite-Branching Datatype Definitions*}
theory InfDatatype imports Datatype_ZF Univ Finite Cardinal_AC begin
--- a/src/ZF/IntDiv_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/IntDiv_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -27,7 +27,7 @@
else negateSnd (posDivAlg (~a,~b));
*)
-header{*The Division Operators Div and Mod*}
+section{*The Division Operators Div and Mod*}
theory IntDiv_ZF
imports Bin OrderArith
--- a/src/ZF/Int_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Int_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
*)
-header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
+section{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
theory Int_ZF imports EquivClass ArithSimp begin
--- a/src/ZF/List_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/List_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Lists in Zermelo-Fraenkel Set Theory*}
+section{*Lists in Zermelo-Fraenkel Set Theory*}
theory List_ZF imports Datatype_ZF ArithSimp begin
--- a/src/ZF/Main_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Main_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -1,4 +1,4 @@
-header{*Theory Main: Everything Except AC*}
+section{*Theory Main: Everything Except AC*}
theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
--- a/src/ZF/Nat_ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Nat_ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*The Natural numbers As a Least Fixed Point*}
+section{*The Natural numbers As a Least Fixed Point*}
theory Nat_ZF imports OrdQuant Bool begin
--- a/src/ZF/OrdQuant.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/OrdQuant.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Authors: Krzysztof Grabczewski and L C Paulson
*)
-header {*Special quantifiers*}
+section {*Special quantifiers*}
theory OrdQuant imports Ordinal begin
--- a/src/ZF/Order.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Order.thy Sun Nov 02 16:39:54 2014 +0100
@@ -7,7 +7,7 @@
Additional definitions and lemmas for reflexive orders.
*)
-header{*Partial and Total Orderings: Basic Definitions and Properties*}
+section{*Partial and Total Orderings: Basic Definitions and Properties*}
theory Order imports WF Perm begin
--- a/src/ZF/OrderArith.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/OrderArith.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
+section{*Combining Orderings: Foundations of Ordinal Arithmetic*}
theory OrderArith imports Order Sum Ordinal begin
--- a/src/ZF/OrderType.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/OrderType.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Order Types and Ordinal Arithmetic*}
+section{*Order Types and Ordinal Arithmetic*}
theory OrderType imports OrderArith OrdQuant Nat_ZF begin
--- a/src/ZF/Ordinal.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Ordinal.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Transitive Sets and Ordinals*}
+section{*Transitive Sets and Ordinals*}
theory Ordinal imports WF Bool equalities begin
--- a/src/ZF/Perm.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Perm.thy Sun Nov 02 16:39:54 2014 +0100
@@ -8,7 +8,7 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-header{*Injections, Surjections, Bijections, Composition*}
+section{*Injections, Surjections, Bijections, Composition*}
theory Perm imports func begin
--- a/src/ZF/QPair.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/QPair.thy Sun Nov 02 16:39:54 2014 +0100
@@ -8,7 +8,7 @@
is not a limit ordinal?
*)
-header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
+section{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
theory QPair imports Sum func begin
--- a/src/ZF/QUniv.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/QUniv.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
*)
-header{*A Small Universe for Lazy Recursive Types*}
+section{*A Small Universe for Lazy Recursive Types*}
theory QUniv imports Univ QPair begin
--- a/src/ZF/Sum.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Sum.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
*)
-header{*Disjoint Sums*}
+section{*Disjoint Sums*}
theory Sum imports Bool equalities begin
--- a/src/ZF/Trancl.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Trancl.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1992 University of Cambridge
*)
-header{*Relations: Their General Properties and Transitive Closure*}
+section{*Relations: Their General Properties and Transitive Closure*}
theory Trancl imports Fixedpt Perm begin
--- a/src/ZF/UNITY/AllocBase.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2001 University of Cambridge
*)
-header{*Common declarations for Chandy and Charpentier's Allocator*}
+section{*Common declarations for Chandy and Charpentier's Allocator*}
theory AllocBase imports Follows MultisetSum Guar begin
--- a/src/ZF/UNITY/Comp.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Comp.thy Sun Nov 02 16:39:54 2014 +0100
@@ -13,7 +13,7 @@
*)
-header{*Composition*}
+section{*Composition*}
theory Comp imports Union Increasing begin
--- a/src/ZF/UNITY/Constrains.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Constrains.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2001 University of Cambridge
*)
-header{*Weak Safety Properties*}
+section{*Weak Safety Properties*}
theory Constrains
imports UNITY
--- a/src/ZF/UNITY/FP.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/FP.thy Sun Nov 02 16:39:54 2014 +0100
@@ -7,7 +7,7 @@
Theory ported from HOL.
*)
-header{*Fixed Point of a Program*}
+section{*Fixed Point of a Program*}
theory FP imports UNITY begin
--- a/src/ZF/UNITY/Follows.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Follows.thy Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
Theory ported from HOL.
*)
-header{*The "Follows" relation of Charpentier and Sivilotte*}
+section{*The "Follows" relation of Charpentier and Sivilotte*}
theory Follows imports SubstAx Increasing begin
--- a/src/ZF/UNITY/GenPrefix.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
Based on Lex/Prefix
*)
-header{*Charpentier's Generalized Prefix Relation*}
+section{*Charpentier's Generalized Prefix Relation*}
theory GenPrefix
imports Main
--- a/src/ZF/UNITY/Guar.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Guar.thy Sun Nov 02 16:39:54 2014 +0100
@@ -19,7 +19,7 @@
*)
-header{*The Chandy-Sanders Guarantees Operator*}
+section{*The Chandy-Sanders Guarantees Operator*}
theory Guar imports Comp begin
--- a/src/ZF/UNITY/Increasing.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Increasing.thy Sun Nov 02 16:39:54 2014 +0100
@@ -6,7 +6,7 @@
relation r over the domain A.
*)
-header{*Charpentier's "Increasing" Relation*}
+section{*Charpentier's "Increasing" Relation*}
theory Increasing imports Constrains Monotonicity begin
--- a/src/ZF/UNITY/Monotonicity.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy Sun Nov 02 16:39:54 2014 +0100
@@ -6,7 +6,7 @@
set relations.
*)
-header{*Monotonicity of an Operator WRT a Relation*}
+section{*Monotonicity of an Operator WRT a Relation*}
theory Monotonicity imports GenPrefix MultisetSum
begin
--- a/src/ZF/UNITY/MultisetSum.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/MultisetSum.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
Author: Sidi O Ehmety
*)
-header {*Setsum for Multisets*}
+section {*Setsum for Multisets*}
theory MultisetSum
imports "../Induct/Multiset"
--- a/src/ZF/UNITY/Mutex.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/Mutex.thy Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
reduce to the empty set.
*)
-header{*Mutual Exclusion*}
+section{*Mutual Exclusion*}
theory Mutex
imports SubstAx
--- a/src/ZF/UNITY/State.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/State.thy Sun Nov 02 16:39:54 2014 +0100
@@ -8,7 +8,7 @@
- variables can be quantified over.
*)
-header{*UNITY Program States*}
+section{*UNITY Program States*}
theory State imports Main begin
--- a/src/ZF/UNITY/SubstAx.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
Theory ported from HOL.
*)
-header{*Weak LeadsTo relation (restricted to the set of reachable states)*}
+section{*Weak LeadsTo relation (restricted to the set of reachable states)*}
theory SubstAx
imports WFair Constrains
--- a/src/ZF/UNITY/UNITY.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/UNITY.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2001 University of Cambridge
*)
-header {*The Basic UNITY Theory*}
+section {*The Basic UNITY Theory*}
theory UNITY imports State begin
--- a/src/ZF/UNITY/WFair.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/UNITY/WFair.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1998 University of Cambridge
*)
-header{*Progress under Weak Fairness*}
+section{*Progress under Weak Fairness*}
theory WFair
imports UNITY Main_ZFC
--- a/src/ZF/Univ.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Univ.thy Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
But Ind_Syntax.univ refers to the constant "Univ.univ"
*)
-header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
+section{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
theory Univ imports Epsilon Cardinal begin
--- a/src/ZF/WF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/WF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -14,7 +14,7 @@
a mess.
*)
-header{*Well-Founded Recursion*}
+section{*Well-Founded Recursion*}
theory WF imports Trancl begin
--- a/src/ZF/ZF.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ZF.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
*)
-header{*Zermelo-Fraenkel Set Theory*}
+section{*Zermelo-Fraenkel Set Theory*}
theory ZF
imports "~~/src/FOL/FOL"
--- a/src/ZF/Zorn.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/Zorn.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header{*Zorn's Lemma*}
+section{*Zorn's Lemma*}
theory Zorn imports OrderArith AC Inductive_ZF begin
--- a/src/ZF/document/root.tex Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/document/root.tex Sun Nov 02 16:39:54 2014 +0100
@@ -25,8 +25,7 @@
\newpage
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
\parindent 0pt\parskip 0.5ex
--- a/src/ZF/equalities.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/equalities.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1992 University of Cambridge
*)
-header{*Basic Equalities and Inclusions*}
+section{*Basic Equalities and Inclusions*}
theory equalities imports pair begin
--- a/src/ZF/ex/CoUnit.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/CoUnit.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-header {* Trivial codatatype definitions, one of which goes wrong! *}
+section {* Trivial codatatype definitions, one of which goes wrong! *}
theory CoUnit imports Main begin
--- a/src/ZF/ex/Group.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/Group.thy Sun Nov 02 16:39:54 2014 +0100
@@ -1,6 +1,6 @@
(* Title: ZF/ex/Group.thy *)
-header {* Groups *}
+section {* Groups *}
theory Group imports Main begin
--- a/src/ZF/ex/Primes.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/Primes.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1996 University of Cambridge
*)
-header{*The Divides Relation and Euclid's algorithm for the GCD*}
+section{*The Divides Relation and Euclid's algorithm for the GCD*}
theory Primes imports Main begin
--- a/src/ZF/ex/Ring.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/Ring.thy Sun Nov 02 16:39:54 2014 +0100
@@ -2,7 +2,7 @@
*)
-header {* Rings *}
+section {* Rings *}
theory Ring imports Group begin
--- a/src/ZF/ex/misc.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/ex/misc.thy Sun Nov 02 16:39:54 2014 +0100
@@ -5,7 +5,7 @@
Composition of homomorphisms, Pastre's examples, ...
*)
-header{*Miscellaneous ZF Examples*}
+section{*Miscellaneous ZF Examples*}
theory misc imports Main begin
--- a/src/ZF/func.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/func.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1991 University of Cambridge
*)
-header{*Functions, Function Spaces, Lambda-Abstraction*}
+section{*Functions, Function Spaces, Lambda-Abstraction*}
theory func imports equalities Sum begin
--- a/src/ZF/pair.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/pair.thy Sun Nov 02 16:39:54 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1992 University of Cambridge
*)
-header{*Ordered Pairs*}
+section{*Ordered Pairs*}
theory pair imports upair
begin
--- a/src/ZF/upair.thy Sun Nov 02 16:09:35 2014 +0100
+++ b/src/ZF/upair.thy Sun Nov 02 16:39:54 2014 +0100
@@ -9,7 +9,7 @@
Ordered pairs and descriptions are defined using cons ("set notation")
*)
-header{*Unordered Pairs*}
+section{*Unordered Pairs*}
theory upair
imports ZF