| changeset 16924 | 04246269386e |
| parent 16775 | c1b87ef4a1c3 |
| child 17318 | bc1c75855f3d |
--- a/src/HOL/Hyperreal/Integration.thy Tue Jul 26 18:31:18 2005 +0200 +++ b/src/HOL/Hyperreal/Integration.thy Wed Jul 27 11:28:18 2005 +0200 @@ -361,7 +361,7 @@ apply (drule spec)+ apply auto apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1]) -apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric]) +apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric]) done text{*Fundamental theorem of calculus (Part I)*}