--- a/src/HOL/Computational_Algebra/Nth_Powers.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Sat Nov 11 18:41:08 2017 +0000
@@ -111,9 +111,10 @@
ultimately show "n dvd multiplicity p a"
by (auto simp: not_dvd_imp_multiplicity_0)
qed
- from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
- from A[of b a] assms show "is_nth_power n b"
- by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
+ from A [of a b] assms show "is_nth_power n a"
+ by (cases "n = 0") simp_all
+ from A [of b a] assms show "is_nth_power n b"
+ by (cases "n = 0") (simp_all add: ac_simps)
qed
lemma is_nth_power_mult_coprime_nat_iff: