--- a/src/HOL/Library/Extended_Nat.thy Tue Jul 26 14:05:28 2011 +0200 +++ b/src/HOL/Library/Extended_Nat.thy Tue Jul 26 14:50:15 2011 +0200 @@ -564,6 +564,7 @@ qed (simp_all add: inf_enat_def sup_enat_def) end +instance enat :: complete_linorder .. subsection {* Traditional theorem names *}