--- a/src/HOL/Library/Extended_Nat.thy Mon Dec 08 12:30:47 2014 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Mon Dec 08 14:32:11 2014 +0100
@@ -6,7 +6,7 @@
section {* Extended natural numbers (i.e. with infinity) *}
theory Extended_Nat
-imports Main Countable
+imports Complex_Main Countable
begin
class infinity =
@@ -615,8 +615,6 @@
subsection {* Complete Lattice *}
-text {* TODO: enat as order topology? *}
-
instantiation enat :: complete_lattice
begin
@@ -649,6 +647,17 @@
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