1.1 --- a/src/HOL/Hyperreal/Lim.ML	Mon Oct 07 19:01:51 2002 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.ML	Tue Oct 08 08:20:17 2002 +0200
     1.3 @@ -877,7 +877,6 @@
     1.4       approx_mult1 1);
     1.5  by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
     1.6  by (subgoal_tac "(*f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
     1.7 -by (rotate_tac ~1 2);
     1.8  by (auto_tac (claset(),
     1.9      simpset() addsimps [real_diff_def, hypreal_diff_def, 
    1.10  		(approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),