src/HOL/NthRoot.thy
changeset 35216 7641e8d831d2
parent 31880 6fb86c61747c
child 44289 d81d09cdab9c
     1.1 --- a/src/HOL/NthRoot.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/NthRoot.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -566,7 +566,7 @@
     1.4  done
     1.5  
     1.6  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
     1.7 -by (simp add: divide_less_eq mult_compare_simps)
     1.8 +by (simp add: divide_less_eq)
     1.9  
    1.10  lemma four_x_squared: 
    1.11    fixes x::real