--- a/src/HOL/Library/Extended_Nat.thy Tue Jul 26 12:44:36 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Tue Jul 26 13:50:03 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 *}