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