changeset 16775 | c1b87ef4a1c3 |
parent 15140 | 322485b816ac |
child 18585 | 5d379fe2eb74 |
--- a/src/HOL/Hyperreal/NthRoot.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Tue Jul 12 17:56:03 2005 +0200 @@ -115,7 +115,7 @@ lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" apply (simp (no_asm) add: right_distrib) apply (rule add_less_cancel_left [of "-r", THEN iffD1]) -apply (auto intro: mult_pos +apply (auto intro: mult_pos_pos simp add: add_assoc [symmetric] neg_less_0_iff_less) done