src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Wed Jan 28 11:02:11 2009 +0100
+++ b/src/HOL/Nat.thy	Wed Jan 28 11:02:12 2009 +0100
@@ -425,6 +425,17 @@
 
 end
 
+instantiation nat :: bot
+begin
+
+definition bot_nat :: nat where
+  "bot_nat = 0"
+
+instance proof
+qed (simp add: bot_nat_def)
+
+end
+
 subsubsection {* Introduction properties *}
 
 lemma lessI [iff]: "n < Suc n"