src/HOL/NthRoot.thy
changeset 44349 f057535311c5
parent 44320 33439faadd67
child 49753 a344f1a21211
     1.1 --- a/src/HOL/NthRoot.thy	Sat Aug 20 13:07:00 2011 -0700
     1.2 +++ b/src/HOL/NthRoot.thy	Sat Aug 20 15:54:26 2011 -0700
     1.3 @@ -629,7 +629,7 @@
     1.4  apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
     1.5  apply (erule_tac [2] lemma_real_divide_sqrt_less)
     1.6  apply (rule power2_le_imp_le)
     1.7 -apply (auto simp add: real_0_le_divide_iff power_divide)
     1.8 +apply (auto simp add: zero_le_divide_iff power_divide)
     1.9  apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
    1.10  apply (rule add_mono)
    1.11  apply (auto simp add: four_x_squared intro: power_mono)