diff -r c898fdd6ff2d -r 59a68ed9f2f2 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Dec 14 16:08:09 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Dec 14 18:10:38 2006 +0100
@@ -17,8 +17,21 @@
   hypnat_of_nat :: "nat => nat star" where
   "hypnat_of_nat == star_of"
 
+definition
+  hSuc :: "hypnat => hypnat" where
+  hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
+
 subsection{*Properties Transferred from Naturals*}
 
+lemma hSuc_not_zero [iff]: "\<And>m. hSuc m \<noteq> 0"
+by transfer (rule Suc_not_Zero)
+
+lemma zero_not_hSuc [iff]: "\<And>m. 0 \<noteq> hSuc m"
+by transfer (rule Zero_not_Suc)
+
+lemma hSuc_hSuc_eq [iff]: "\<And>m n. (hSuc m = hSuc n) = (m = n)"
+by transfer (rule Suc_Suc_eq)
+
 lemma hypnat_minus_zero [simp]: "!!z. z - z = (0::hypnat)"
 by transfer (rule diff_self_eq_0)