# HG changeset patch
# User haftmann
# Date 1247561803 -7200
# Node ID fafefd0b341cd4d884538a96adf79f18e1adb24e
# Parent  1d93369079c4a635ac6344c934655a837edaa079# Parent  6f07563dc8a97b15b4c923c367d8c87b9657f571
merged

diff -r 6f07563dc8a9 -r fafefd0b341c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Jul 14 10:54:54 2009 +0200
+++ b/src/HOL/GCD.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -1503,7 +1503,7 @@
 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
 
 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
-by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
+by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
 
 
 subsection {* Primes *}