enat is a complete_linorder instance
authorhoelzl
Tue Jul 26 13:50:03 2011 +0200 (2011-07-26)
changeset 43978da7d04d4023c
parent 43977 0eb2b12bd99e
child 43980 995c2534c3fe
enat is a complete_linorder instance
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 26 12:44:36 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 26 13:50:03 2011 +0200
     1.3 @@ -564,6 +564,7 @@
     1.4  qed (simp_all add: inf_enat_def sup_enat_def)
     1.5  end
     1.6  
     1.7 +instance enat :: complete_linorder ..
     1.8  
     1.9  subsection {* Traditional theorem names *}
    1.10