diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -506,9 +506,7 @@
 qed
 
 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
-apply auto
-apply (rule OrderedGroup.add_right_cancel [of _ "-y", THEN iffD1], auto)
-done
+by auto
 
 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
 by auto