diff -r 6c4fd0b4b63a -r 3377a830b727 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Sun Oct 01 18:29:26 2006 +0200 +++ b/src/HOL/Library/Ramsey.thy Sun Oct 01 18:29:28 2006 +0200 @@ -5,7 +5,7 @@ header "Ramsey's Theorem" -theory Ramsey imports Main begin +theory Ramsey imports Main Infinite_Set begin subsection{*Preliminaries*} @@ -138,13 +138,12 @@ then obtain n where "x = ?gt n" .. with pg [of n] show "x \ {..s' \ range ?gt. infinite (?gt -` {s'})" - by (rule inf_img_fin_dom [OF _ nat_infinite]) - (simp add: finite_nat_iff_bounded rangeg) + have "finite (range ?gt)" + by (simp add: finite_nat_iff_bounded rangeg) then obtain s' and n' - where s': "s' = ?gt n'" - and infeqs': "infinite {n. ?gt n = s'}" - by (auto simp add: vimage_def) + where s': "s' = ?gt n'" + and infeqs': "infinite {n. ?gt n = s'}" + by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite) with pg [of n'] have less': "s' bool" - "disj_wf(r) == \T. \n::nat. (\iiT. \n::nat. (\ii 'a, nat => ('a*'a)set, nat set] => nat" - "transition_idx s T A == - LEAST k. \i j. A = {i,j} & i T k" + "transition_idx s T A = + (LEAST k. \i j. A = {i,j} & i T k)" lemma transition_idx_less: