src/HOL/Number_Theory/Primes.thy
changeset 55337 5d45fb978d5a
parent 55242 413ec965f95d
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 11:47:56 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 17:06:11 2014 +0000
     1.3 @@ -31,7 +31,6 @@
     1.4  imports "~~/src/HOL/GCD"
     1.5  begin
     1.6  
     1.7 -declare One_nat_def [simp]
     1.8  declare [[coercion int]]
     1.9  declare [[coercion_enabled]]
    1.10  
    1.11 @@ -408,9 +407,7 @@
    1.12    let ?q2 = "v * y1 + u * x2"
    1.13    from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
    1.14    have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
    1.15 -    apply (auto simp add: algebra_simps) 
    1.16 -    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
    1.17 -    done
    1.18 +    by algebra+
    1.19    thus ?thesis by blast
    1.20  qed
    1.21