Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
1.1 --- a/src/HOL/Library/Infinite_Set.thy Fri Nov 29 08:26:45 2013 +0100
1.2 +++ b/src/HOL/Library/Infinite_Set.thy Fri Nov 29 14:24:21 2013 +0100
1.3 @@ -5,7 +5,7 @@
1.4 header {* Infinite Sets and Related Concepts *}
1.5
1.6 theory Infinite_Set
1.7 -imports Set_Interval
1.8 +imports Main
1.9 begin
1.10
1.11 subsection "Infinite Sets"
1.12 @@ -554,3 +554,4 @@
1.13 by (simp add: atmost_one_def)
1.14
1.15 end
1.16 +