
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"




