src/HOL/Nat.thy
changeset 51329 4a3c453f99a1
parent 51263 31e786e0e6a7
child 52289 83ce5d2841e7
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 20 12:04:42 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 20 12:04:42 2013 +0100
     1.3 @@ -455,6 +455,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance nat :: no_top
     1.8 +  by default (auto intro: less_Suc_eq_le[THEN iffD2])
     1.9 +
    1.10  subsubsection {* Introduction properties *}
    1.11  
    1.12  lemma lessI [iff]: "n < Suc n"