diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Apr 22 13:26:47 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Apr 23 11:04:07 2004 +0200
@@ -139,14 +139,14 @@
 subsection{*Hypernat Addition*}
 
 lemma hypnat_add_congruent2:
-     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
-apply (simp add: congruent2_def, auto, ultra)
-done
+     "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
+by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_add:
   "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypnat(hypnatrel``{%n. X n + Y n})"
-by (simp add: hypnat_add_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_add_congruent2])
+by (simp add: hypnat_add_def 
+    UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_add_congruent2])
 
 lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
 apply (cases z, cases w)
@@ -173,14 +173,14 @@
 
 
 lemma hypnat_minus_congruent2:
-    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
-apply (simp add: congruent2_def, auto, ultra)
-done
+    "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
+by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_minus:
   "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypnat(hypnatrel``{%n. X n - Y n})"
-by (simp add: hypnat_minus_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_minus_congruent2])
+by (simp add: hypnat_minus_def 
+  UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_minus_congruent2])
 
 lemma hypnat_minus_zero: "z - z = (0::hypnat)"
 apply (cases z)
@@ -241,18 +241,17 @@
 subsection{*Hyperreal Multiplication*}
 
 lemma hypnat_mult_congruent2:
-    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
+    "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
 by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_mult:
   "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypnat(hypnatrel``{%n. X n * Y n})"
-by (simp add: hypnat_mult_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_mult_congruent2])
+by (simp add: hypnat_mult_def
+   UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_mult_congruent2])
 
 lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
-apply (cases z, cases w)
-apply (simp add: hypnat_mult mult_ac)
-done
+by (cases z, cases w, simp add: hypnat_mult mult_ac)
 
 lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
 apply (cases z1, cases z2, cases z3)
@@ -797,11 +796,6 @@
 val hypnat_omega_def = thm"hypnat_omega_def";
 
 val hypnatrel_iff = thm "hypnatrel_iff";
-val hypnatrel_refl = thm "hypnatrel_refl";
-val hypnatrel_sym = thm "hypnatrel_sym";
-val hypnatrel_trans = thm "hypnatrel_trans";
-val equiv_hypnatrel = thm "equiv_hypnatrel";
-val equiv_hypnatrel_iff = thms "equiv_hypnatrel_iff";
 val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat";
 val inj_on_Abs_hypnat = thm "inj_on_Abs_hypnat";
 val inj_Rep_hypnat = thm "inj_Rep_hypnat";
@@ -809,7 +803,6 @@
 val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
 val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
 val eq_Abs_hypnat = thm "eq_Abs_hypnat";
-val hypnat_add_congruent2 = thm "hypnat_add_congruent2";
 val hypnat_add = thm "hypnat_add";
 val hypnat_add_commute = thm "hypnat_add_commute";
 val hypnat_add_assoc = thm "hypnat_add_assoc";