# HG changeset patch # User berghofe # Date 1247504825 -7200 # Node ID 1d93369079c4a635ac6344c934655a837edaa079 # Parent 8f37cf60b8852a6f5f1b8dd1885db667860d250e Tuned proof of lcm_1_iff_int, because metis produced enormous proof term. diff -r 8f37cf60b885 -r 1d93369079c4 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Sun Jul 12 14:48:01 2009 +0200 +++ b/src/HOL/GCD.thy Mon Jul 13 19:07:05 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 \ (m=1 \ m = -1) \ (n=1 \ 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 *}