1.1 --- a/src/HOL/Power.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4  apply (auto simp add: power_Suc abs_mult)
     1.5  done
     1.6  
     1.7 -lemma zero_less_power_abs_iff [simp]:
     1.8 +lemma zero_less_power_abs_iff [simp,noatp]:
     1.9       "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
    1.10  proof (induct "n")
    1.11    case 0