src/HOL/Library/Ramsey.thy
 changeset 22665 cf152ff55d16 parent 22367 6860f09242bf child 24853 aab5798e5a33
```     1.1 --- a/src/HOL/Library/Ramsey.thy	Fri Apr 13 21:26:34 2007 +0200
1.2 +++ b/src/HOL/Library/Ramsey.thy	Fri Apr 13 21:26:35 2007 +0200
1.3 @@ -7,10 +7,9 @@
1.4
1.5  theory Ramsey imports Main Infinite_Set begin
1.6
1.7 +subsection {* Preliminaries *}
1.8
1.9 -subsection{*Preliminaries*}
1.10 -
1.11 -subsubsection{*``Axiom'' of Dependent Choice*}
1.12 +subsubsection {* ``Axiom'' of Dependent Choice *}
1.13
1.14  consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
1.15    --{*An integer-indexed chain of choices*}
1.16 @@ -50,7 +49,7 @@
1.17  qed
1.18
1.19
1.20 -subsubsection {*Partitions of a Set*}
1.21 +subsubsection {* Partitions of a Set *}
1.22
1.23  definition
1.24    part :: "nat => nat => 'a set => ('a set => nat) => bool"
1.25 @@ -72,7 +71,7 @@
1.26    unfolding part_def by blast
1.27
1.28
1.29 -subsection {*Ramsey's Theorem: Infinitary Version*}
1.30 +subsection {* Ramsey's Theorem: Infinitary Version *}
1.31
1.32  lemma Ramsey_induction:
1.33    fixes s and r::nat
1.34 @@ -231,9 +230,7 @@
1.35  qed
1.36
1.37
1.38 -
1.39 -
1.40 -subsection {*Disjunctive Well-Foundedness*}
1.41 +subsection {* Disjunctive Well-Foundedness *}
1.42
1.43  text {*
1.44    An application of Ramsey's theorem to program termination. See
1.45 @@ -336,5 +333,4 @@
1.46    thus False using wfT less by blast
1.47  qed
1.48
1.49 -
1.50  end
```