# HG changeset patch
# User hoelzl
# Date 1311681003 -7200
# Node ID da7d04d4023cd851b324ccb44f916a44ffe0f29d
# Parent  0eb2b12bd99e5af3e8d04fb8d78bed14285cc00e
enat is a complete_linorder instance

diff -r 0eb2b12bd99e -r da7d04d4023c src/HOL/Library/Extended_Nat.thy
--- 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 *}