src/HOL/GCD.thy
changeset 66796 ea9b2e5ca9fc
parent 65811 2653f1cd8775
child 66803 dd8922885a68
     1.1 --- a/src/HOL/GCD.thy	Sun Oct 08 22:28:19 2017 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:19 2017 +0200
     1.3 @@ -1995,11 +1995,7 @@
     1.4  
     1.5  lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
     1.6    for k m n :: int
     1.7 -  apply (subst (1 2) gcd_abs_int)
     1.8 -  apply (subst (1 2) abs_mult)
     1.9 -  apply (rule gcd_mult_distrib_nat [transferred])
    1.10 -    apply auto
    1.11 -  done
    1.12 +  by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
    1.13  
    1.14  lemma coprime_crossproduct_nat:
    1.15    fixes a b c d :: nat
    1.16 @@ -2480,10 +2476,7 @@
    1.17  
    1.18  lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
    1.19    for m n :: int
    1.20 -  apply (subst lcm_abs_int)
    1.21 -  apply (rule lcm_pos_nat [transferred])
    1.22 -     apply auto
    1.23 -  done
    1.24 +  by (simp add: lcm_int_def lcm_pos_nat)
    1.25  
    1.26  lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
    1.27    for m n :: nat