diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -145,45 +145,15 @@
 
 
 lemma hypnat_of_nat_def: "hypnat_of_nat m == of_nat m"
-by (transfer star_of_nat_def) simp
-
-lemma hypnat_of_nat_add:
-      "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
-by simp
-
-lemma hypnat_of_nat_mult:
-      "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
-by simp
-
-lemma hypnat_of_nat_less_iff:
-      "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
-by simp
-
-lemma hypnat_of_nat_le_iff:
-      "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
-by simp
-
-lemma hypnat_of_nat_eq_iff:
-      "(hypnat_of_nat z = hypnat_of_nat w) = (z = w)"
-by simp
+by (transfer, simp)
 
 lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
 by simp
 
-lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
-by simp
-
-lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
-by simp
-
 lemma hypnat_of_nat_Suc [simp]:
      "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
 by (simp add: hypnat_of_nat_def)
 
-lemma hypnat_of_nat_minus:
-      "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
-by simp
-
 
 subsection{*Existence of an infinite hypernatural number*}
 
@@ -217,9 +187,7 @@
 
 lemma hypnat_of_nat_eq:
      "hypnat_of_nat m  = star_n (%n::nat. m)"
-apply (induct m) 
-apply (simp_all add: star_n_zero_num star_n_one_num star_n_add)
-done
+by (simp add: star_of_def)
 
 lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
 by (force simp add: hypnat_of_nat_def Nats_def) 
@@ -436,7 +404,6 @@
 
 val starrel_iff = thm "starrel_iff";
 val lemma_starrel_refl = thm "lemma_starrel_refl";
-val eq_Abs_star = thm "eq_Abs_star";
 val hypnat_minus_zero = thm "hypnat_minus_zero";
 val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
 val hypnat_add_is_0 = thm "hypnat_add_is_0";
@@ -461,16 +428,8 @@
 val hypnat_neq0_conv = thm "hypnat_neq0_conv";
 val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
 val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
-val hypnat_of_nat_add = thm "hypnat_of_nat_add";
-val hypnat_of_nat_minus = thm "hypnat_of_nat_minus";
-val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
-val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
-val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
-val hypnat_of_nat_eq = thm"hypnat_of_nat_eq"
 val SHNat_eq = thm"SHNat_eq"
 val hypnat_of_nat_one = thm "hypnat_of_nat_one";
-val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
-val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
 val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
 val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
 val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";