src/HOL/Number_Theory/Primes.thy

 
 theory Primes
 imports "~~/src/HOL/GCD"
 begin
 
-declare One_nat_def [simp]
 declare [[coercion int]]
 declare [[coercion_enabled]]
 
 definition prime :: "nat \<Rightarrow> bool"
   where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"

   let ?x = "v * a * x1 + u * b * x2"
   let ?q1 = "v * x1 + u * y2"
   let ?q2 = "v * y1 + u * x2"
   from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
-    apply (auto simp add: algebra_simps) 
-    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
-    done
+    by algebra+
   thus ?thesis by blast
 qed
 
 text {* Primality *}