--- 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)
--- 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"