# HG changeset patch
# User paulson
# Date 971346390 -7200
# Node ID b52140d1a7bc29a31e19c48f9bd4549cacd0c5b5
# Parent  abdab72b8c7ae8ce46d502dadc444c0eda8a5e06
tidied

diff -r abdab72b8c7a -r b52140d1a7bc src/HOL/Real/Hyperreal/HyperNat.ML
--- a/src/HOL/Real/Hyperreal/HyperNat.ML	Thu Oct 12 12:19:15 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperNat.ML	Thu Oct 12 12:26:30 2000 +0200
@@ -134,7 +134,7 @@
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_add_congruent2";
 
@@ -188,7 +188,7 @@
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_minus_congruent2";
  
@@ -279,7 +279,7 @@
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_mult_congruent2";