changeset 35216 | 7641e8d831d2 |
parent 35028 | 108662d50512 |
child 35828 | 46cfc4b8112e |
--- a/src/HOL/Power.thy Thu Feb 18 13:29:59 2010 -0800 +++ b/src/HOL/Power.thy Thu Feb 18 14:21:44 2010 -0800 @@ -332,7 +332,7 @@ lemma abs_power_minus [simp]: "abs ((-a) ^ n) = abs (a ^ n)" - by (simp add: abs_minus_cancel power_abs) + by (simp add: power_abs) lemma zero_less_power_abs_iff [simp, noatp]: "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"