author | Andreas Lochbihler |
Tue, 26 Jul 2011 14:50:15 +0200 | |
changeset 44851 | 995c2534c3fe |
parent 44850 | 9f27d2bf4087 |
parent 44849 | da7d04d4023c |
child 44852 | 404ae49ce29f |
1.1 --- a/src/HOL/Library/Extended_Nat.thy Tue Jul 26 14:05:28 2011 +0200 1.2 +++ b/src/HOL/Library/Extended_Nat.thy Tue Jul 26 14:50:15 2011 +0200 1.3 @@ -564,6 +564,7 @@ 1.4 qed (simp_all add: inf_enat_def sup_enat_def) 1.5 end 1.6 1.7 +instance enat :: complete_linorder .. 1.8 1.9 subsection {* Traditional theorem names *} 1.10