--- a/src/HOL/Number_Theory/Primes.thy Wed Feb 05 11:47:56 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Wed Feb 05 17:06:11 2014 +0000
@@ -31,7 +31,6 @@
imports "~~/src/HOL/GCD"
begin
-declare One_nat_def [simp]
declare [[coercion int]]
declare [[coercion_enabled]]
@@ -408,9 +407,7 @@
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