diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/Power.thy	Wed Oct 09 14:51:54 2019 +0000
@@ -123,8 +123,9 @@
 context comm_monoid_mult
 begin
 
-lemma power_mult_distrib [field_simps]: "(a * b) ^ n = (a ^ n) * (b ^ n)"
-  by (induct n) (simp_all add: ac_simps)
+lemma power_mult_distrib [algebra_simps, algebra_split_simps, field_simps, field_split_simps, divide_simps]:
+  "(a * b) ^ n = (a ^ n) * (b ^ n)"
+  by (induction n) (simp_all add: ac_simps)
 
 end
 
@@ -378,7 +379,7 @@
 begin
 
 text \<open>Perhaps these should be simprules.\<close>
-lemma power_inverse [field_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)"
+lemma power_inverse [field_simps, field_split_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)"
 proof (cases "a = 0")
   case True
   then show ?thesis by (simp add: power_0_left)
@@ -389,7 +390,7 @@
   then show ?thesis by simp
 qed
 
-lemma power_one_over [field_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n"
+lemma power_one_over [field_simps, field_split_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n"
   using power_inverse [of a] by (simp add: divide_inverse)
 
 end
@@ -397,7 +398,7 @@
 context field
 begin
 
-lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
+lemma power_divide [field_simps, field_split_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
   by (induct n) simp_all
 
 end