# HG changeset patch
# User haftmann
# Date 1233136932 -3600
# Node ID f4c6e546b7fe6e586847f42477d1c6b399e23af9
# Parent  16a19466bf814d9518345fb3cee295f3d5a4f3e5
nat is a bot instance

diff -r 16a19466bf81 -r f4c6e546b7fe src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Wed Jan 28 11:02:11 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Wed Jan 28 11:02:12 2009 +0100
@@ -8,17 +8,6 @@
 imports Plain "~~/src/HOL/Presburger"
 begin
 
-text {* FIXME: move to Nat.thy *}
-
-instantiation nat :: bot
-begin
-
-definition bot_nat :: nat where
-  "bot_nat = 0"
-
-instance proof
-qed (simp add: bot_nat_def)
-
 subsection {* Type definition *}
 
 text {*
@@ -26,8 +15,6 @@
   infinity.
 *}
 
-end
-
 datatype inat = Fin nat | Infty
 
 notation (xsymbols)
diff -r 16a19466bf81 -r f4c6e546b7fe 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"