merged
authorhaftmann
Tue Jul 14 15:54:51 2009 +0200 (2009-07-14)
changeset 320659fa18f1c2b2d
parent 32064 53ca12ff305d
parent 31996 1d93369079c4
child 32066 091f1e304120
merged
     1.1 --- a/src/HOL/GCD.thy	Tue Jul 14 15:54:19 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Tue Jul 14 15:54:51 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 *}