src/HOL/Library/Extended_Nat.thy
changeset 52729 412c9e0381a1
parent 51717 9e7d1c139569
child 54415 eaf25431d4c4
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -452,7 +452,7 @@
     1.4  apply (erule (1) le_less_trans)
     1.5  done
     1.6  
     1.7 -instantiation enat :: "{bot, top}"
     1.8 +instantiation enat :: "{order_bot, order_top}"
     1.9  begin
    1.10  
    1.11  definition bot_enat :: enat where
    1.12 @@ -623,7 +623,8 @@
    1.13        unfolding Sup_enat_def by (cases "finite A") auto }
    1.14    { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
    1.15        unfolding Sup_enat_def using finite_enat_bounded by auto }
    1.16 -qed (simp_all add: inf_enat_def sup_enat_def)
    1.17 +qed (simp_all add:
    1.18 + inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def)
    1.19  end
    1.20  
    1.21  instance enat :: complete_linorder ..