src/HOL/Number_Theory/Primes.thy
 changeset 57512 cc97b347b301 parent 55337 5d45fb978d5a child 58623 2db1df2c8467
```--- a/src/HOL/Number_Theory/Primes.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -106,7 +106,7 @@
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_nat_def dvd_def apply auto
-  by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
+  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
n_less_n_mult_m one_le_mult_iff less_imp_le_nat)

lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
@@ -209,7 +209,7 @@
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
moreover
{ assume pb: "p dvd b"
-      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+      have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
by auto
with p have "coprime a p"
@@ -323,7 +323,7 @@
moreover
{assume px: "p dvd y"
then obtain d where d: "y = p*d" unfolding dvd_def by blast
-    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
+    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
hence th: "d*x = p^k" using p0 by simp
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
with d have "y = p^Suc i" by simp
@@ -355,7 +355,7 @@
shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
proof
assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
-    unfolding dvd_def  apply (auto simp add: mult_commute) by blast
+    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
from e ij have "p^(i + j) = p^k" by (simp add: power_add)
hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp ```