author | hoelzl |
Tue, 26 Jul 2011 13:50:03 +0200 | |
changeset 44849 | da7d04d4023c |
parent 44848 | 0eb2b12bd99e |
child 44851 | 995c2534c3fe |
1.1 --- a/src/HOL/Library/Extended_Nat.thy Tue Jul 26 12:44:36 2011 +0200 1.2 +++ b/src/HOL/Library/Extended_Nat.thy Tue Jul 26 13:50:03 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