| changeset 30273 | ecd6f0ca62ea |
| parent 28952 | 15a4b2cf8c34 |
| child 31014 | 79f0858d9d49 |
--- a/src/HOL/NthRoot.thy Thu Mar 05 00:16:28 2009 +0100 +++ b/src/HOL/NthRoot.thy Wed Mar 04 17:12:23 2009 -0800 @@ -613,7 +613,7 @@ apply (auto simp add: real_0_le_divide_iff power_divide) apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst]) apply (rule add_mono) -apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono) +apply (auto simp add: four_x_squared intro: power_mono) done text "Legacy theorem names:"