--- a/src/HOL/Hyperreal/Star.ML Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/Star.ML Thu Dec 13 15:45:03 2001 +0100
@@ -193,7 +193,7 @@
-----------------------------------------------------------------------*)
Goalw [congruent_def] "congruent hyprel (%X. hyprel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS(Fuf_tac));
qed "starfun_congruent";
@@ -472,7 +472,7 @@
Goal "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = \
\ (ALL m. {n. abs (X n + - Y n) < \
\ inverse(real(Suc m))} : FreeUltrafilterNat)";
-by (rtac (approx_minus_iff RS ssubst) 1);
+by (stac approx_minus_iff 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (auto_tac (claset(),
simpset() addsimps [hypreal_minus, hypreal_add,