diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Fri Mar 27 10:05:08 2009 +0100 +++ b/src/HOL/Library/Ramsey.thy Fri Mar 27 10:05:11 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/Ramsey.thy - ID: $Id$ Author: Tom Ridge. Converted to structured Isar by L C Paulson *) header "Ramsey's Theorem" theory Ramsey -imports Plain "~~/src/HOL/Presburger" Infinite_Set +imports Main Infinite_Set begin subsection {* Preliminaries *}