diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Library/Float.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -1108,7 +1108,7 @@
   shows "0 \<le> real (lapprox_rat n x y)"
 using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    powr_int[of 2, simplified]
-  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos)
+  by auto
 
 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
   using round_up by (simp add: rapprox_rat_def)