diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -324,10 +324,8 @@
 apply (frule hrabs_less_gt_zero)
 apply (drule_tac x = "r/t" in bspec)
 apply (blast intro: SReal_divide)
-apply (simp add: zero_less_divide_iff)
-apply (case_tac "x=0 | y=0")
-apply (cut_tac [2] a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
-apply (auto simp add: zero_less_divide_iff)
+apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
+apply (auto simp add: times_divide_eq_left zero_less_divide_iff)
 done
 
 lemma Infinitesimal_HFinite_mult2: