# HG changeset patch
# User Andreas Lochbihler
# Date 1311684615 -7200
# Node ID 995c2534c3fe96863d518c3cb691879949be3e6a
# Parent  9f27d2bf408776e253863a246a5346c3eb293601# Parent  da7d04d4023cd851b324ccb44f916a44ffe0f29d
merged

diff -r 9f27d2bf4087 -r 995c2534c3fe src/HOL/Library/Extended_Nat.thy
--- 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 *}