changeset 30738 | 0842e906300c |
parent 28741 | 1b257449f804 |
child 32960 | 69916a850301 |
--- 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 *}