# HG changeset patch
# User chaieb
# Date 1234196424 0
# Node ID 018ac1fa1ed31914fc46d15a9b071cb201326d0d
# Parent  a562ca0c408d1c60f23fd6c13d53ecd10931d773
Imports Main in order to avoid the typerep problem

diff -r a562ca0c408d -r 018ac1fa1ed3 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Feb 09 16:19:46 2009 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Feb 09 16:20:24 2009 +0000
@@ -6,7 +6,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Plain "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
+imports Main "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
 begin