--- a/src/HOL/Library/Extended_Nat.thy Sat Nov 22 11:05:41 2014 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Tue Dec 09 16:22:40 2014 +0100
@@ -6,7 +6,7 @@
section {* Extended natural numbers (i.e. with infinity) *}
theory Extended_Nat
-imports Complex_Main Countable
+imports Main Countable
begin
class infinity =
@@ -647,17 +647,6 @@
instance enat :: complete_linorder ..
-instantiation enat :: linorder_topology
-begin
-
-definition open_enat :: "enat set \<Rightarrow> bool" where
- "open_enat = generate_topology (range lessThan \<union> range greaterThan)"
-
-instance
- proof qed (rule open_enat_def)
-
-end
-
subsection {* Traditional theorem names *}
lemmas enat_defs = zero_enat_def one_enat_def eSuc_def