# HG changeset patch
# User traytel
# Date 1385731461 -3600
# Node ID 7e291ae244ea245e3d7594af0b9720226557ad96
# Parent  31afce809794e0f08272a0ed211113ec980be813
Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>

diff -r 31afce809794 -r 7e291ae244ea src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Nov 29 08:26:45 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Nov 29 14:24:21 2013 +0100
@@ -5,7 +5,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Set_Interval
+imports Main
 begin
 
 subsection "Infinite Sets"
@@ -554,3 +554,4 @@
   by (simp add: atmost_one_def)
 
 end
+