src/HOL/Nat.thy
changeset 29652 f4c6e546b7fe
parent 29608 564ea783ace8
child 29668 33ba3faeaa0e
     1.1 --- a/src/HOL/Nat.thy	Wed Jan 28 11:02:11 2009 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Jan 28 11:02:12 2009 +0100
     1.3 @@ -425,6 +425,17 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation nat :: bot
     1.8 +begin
     1.9 +
    1.10 +definition bot_nat :: nat where
    1.11 +  "bot_nat = 0"
    1.12 +
    1.13 +instance proof
    1.14 +qed (simp add: bot_nat_def)
    1.15 +
    1.16 +end
    1.17 +
    1.18  subsubsection {* Introduction properties *}
    1.19  
    1.20  lemma lessI [iff]: "n < Suc n"