# HG changeset patch
# User haftmann
# Date 1507494499 -7200
# Node ID ea9b2e5ca9fc2c108979851493b8b7f1c5dbe547
# Parent  420d0080545fd9c420fe8a4c1d5b2159ca8c5ac6
tuned proofs

diff -r 420d0080545f -r ea9b2e5ca9fc src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:19 2017 +0200
@@ -1995,11 +1995,7 @@
 
 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
   for k m n :: int
-  apply (subst (1 2) gcd_abs_int)
-  apply (subst (1 2) abs_mult)
-  apply (rule gcd_mult_distrib_nat [transferred])
-    apply auto
-  done
+  by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
 
 lemma coprime_crossproduct_nat:
   fixes a b c d :: nat
@@ -2480,10 +2476,7 @@
 
 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
   for m n :: int
-  apply (subst lcm_abs_int)
-  apply (rule lcm_pos_nat [transferred])
-     apply auto
-  done
+  by (simp add: lcm_int_def lcm_pos_nat)
 
 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
   for m n :: nat