src/HOL/Hyperreal/NthRoot.thy
changeset 25875 536dfdc25e0a
parent 25766 6960410f134d
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Wed Jan 09 19:23:36 2008 +0100
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Jan 09 19:23:50 2008 +0100
     1.3 @@ -328,7 +328,7 @@
     1.4  unfolding isCont_def
     1.5  apply (rule LIM_I)
     1.6  apply (rule_tac x="r ^ n" in exI, safe)
     1.7 -apply (simp add: zero_less_power)
     1.8 +apply (simp)
     1.9  apply (simp add: real_root_abs [symmetric])
    1.10  apply (rule_tac n="n" in power_less_imp_less_base, simp_all)
    1.11  done