changeset 36096 | abc6a2ea4b88 |
parent 35216 | 7641e8d831d2 |
child 44289 | d81d09cdab9c |
--- a/src/HOL/NthRoot.thy Fri Apr 02 13:33:48 2010 +0200 +++ b/src/HOL/NthRoot.thy Wed Apr 07 19:17:10 2010 +0200 @@ -566,7 +566,7 @@ done lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" -by (simp add: divide_less_eq mult_compare_simps) +by (simp add: divide_less_eq) lemma four_x_squared: fixes x::real