src/HOL/Number_Theory/Primes.thy

--- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -64,7 +64,7 @@
 
 lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   apply (unfold prime_def)
-  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
+  apply (metis gcd_dvd1 gcd_dvd2)
   done
 
 lemma prime_int_altdef:
@@ -72,22 +72,22 @@
     m = 1 \<or> m = p))"
   apply (simp add: prime_def)
   apply (auto simp add: )
-  apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
+  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
   apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
   done
 
 lemma prime_imp_coprime_int:
   fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   apply (unfold prime_int_altdef)
-  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
+  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   done
 
 lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
-  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
+  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
 
 lemma prime_dvd_mult_int:
   fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
-  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
+  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
 
 lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
     p dvd m * n = (p dvd m \<or> p dvd n)"
@@ -198,20 +198,20 @@
     { assume pa: "p dvd a"
       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
       with p have "coprime b p"
-        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
+        by (subst gcd.commute, intro prime_imp_coprime_nat)
       then have pnb: "coprime (p^n) b"
-        by (subst gcd_commute_nat, rule coprime_exp_nat)
-      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
+        by (subst gcd.commute, rule coprime_exp_nat)
+      from coprime_dvd_mult[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)
       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
         by auto
       with p have "coprime a p"
-        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
+        by (subst gcd.commute, intro prime_imp_coprime_nat)
       then have pna: "coprime (p^n) a"
-        by (subst gcd_commute_nat, rule coprime_exp_nat)
-      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
+        by (subst gcd.commute, rule coprime_exp_nat)
+      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
     ultimately have ?thesis by blast }
   ultimately show ?thesis by blast
 qed