diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Power.thy --- 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 \ a \ 0 \ n = 0"