changeset 24286 | 7619080e49f0 |
parent 23544 | 4b4165cb3e0d |
child 24376 | e403ab5c9415 |
--- a/src/HOL/Power.thy Wed Aug 15 09:02:11 2007 +0200 +++ b/src/HOL/Power.thy Wed Aug 15 12:52:56 2007 +0200 @@ -183,7 +183,7 @@ apply (auto simp add: power_Suc abs_mult) done -lemma zero_less_power_abs_iff [simp]: +lemma zero_less_power_abs_iff [simp,noatp]: "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)" proof (induct "n") case 0