--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Apr 01 17:02:43 2019 +0100
@@ -319,12 +319,12 @@
proof (cases "even k")
case True
with * \<open>in_carrier ls\<close> show ?thesis
- by (simp add: even_pow sqr_ci nat_pow_distr nat_pow_mult
+ by (simp add: even_pow sqr_ci nat_pow_distrib nat_pow_mult
mult_2 [symmetric] even_two_times_div_two)
next
case False
with * \<open>in_carrier ls\<close> show ?thesis
- by (simp add: odd_pow mul_ci sqr_ci nat_pow_distr nat_pow_mult
+ by (simp add: odd_pow mul_ci sqr_ci nat_pow_distrib nat_pow_mult
mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
qed
qed