diff -r 028edb1e5b99 -r e0237f2eb49d src/HOL/Power.thy --- a/src/HOL/Power.thy Sun Jan 19 14:50:03 2020 +0100 +++ b/src/HOL/Power.thy Tue Jan 21 11:02:27 2020 +0100 @@ -377,7 +377,7 @@ end -context normalization_semidom +context normalization_semidom_multiplicative begin lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"