src/HOL/Library/Extended_Nat.thy
changeset 59115 f65ac77f7e07
parent 59106 af691e67f71f
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Sat Nov 22 11:05:41 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Dec 09 16:22:40 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section {* Extended natural numbers (i.e. with infinity) *}
     1.5  
     1.6  theory Extended_Nat
     1.7 -imports Complex_Main Countable
     1.8 +imports Main Countable
     1.9  begin
    1.10  
    1.11  class infinity =
    1.12 @@ -647,17 +647,6 @@
    1.13  
    1.14  instance enat :: complete_linorder ..
    1.15  
    1.16 -instantiation enat :: linorder_topology
    1.17 -begin
    1.18 -
    1.19 -definition open_enat :: "enat set \<Rightarrow> bool" where
    1.20 -  "open_enat = generate_topology (range lessThan \<union> range greaterThan)"
    1.21 -
    1.22 -instance
    1.23 -  proof qed (rule open_enat_def)
    1.24 -
    1.25 -end
    1.26 -
    1.27  subsection {* Traditional theorem names *}
    1.28  
    1.29  lemmas enat_defs = zero_enat_def one_enat_def eSuc_def