changeset 35216 | 7641e8d831d2 |
parent 31880 | 6fb86c61747c |
child 44289 | d81d09cdab9c |
--- a/src/HOL/NthRoot.thy Thu Feb 18 13:29:59 2010 -0800 +++ b/src/HOL/NthRoot.thy Thu Feb 18 14:21:44 2010 -0800 @@ -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