src/HOL/GCD.thy
changeset 31996 1d93369079c4
parent 31995 8f37cf60b885
child 32007 a2a3685f61c3
child 32040 830141c9e528
     1.1 --- a/src/HOL/GCD.thy	Sun Jul 12 14:48:01 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Jul 13 19:07:05 2009 +0200
     1.3 @@ -1503,7 +1503,7 @@
     1.4  by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
     1.5  
     1.6  lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
     1.7 -by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
     1.8 +by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
     1.9  
    1.10  
    1.11  subsection {* Primes *}