--- a/src/HOL/Nat.thy Wed Feb 20 12:04:42 2013 +0100
+++ b/src/HOL/Nat.thy Wed Feb 20 12:04:42 2013 +0100
@@ -455,6 +455,9 @@
end
+instance nat :: no_top
+ by default (auto intro: less_Suc_eq_le[THEN iffD2])
+
subsubsection {* Introduction properties *}
lemma lessI [iff]: "n < Suc n"