src/HOL/Library/Extended_Nat.thy

   { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
       unfolding Sup_enat_def using finite_enat_bounded by auto }
 qed (simp_all add: inf_enat_def sup_enat_def)
 end
 
+instance enat :: complete_linorder ..
 
 subsection {* Traditional theorem names *}
 
 lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
   plus_enat_def less_eq_enat_def less_enat_def