src/HOL/Number_Theory/Primes.thy
 changeset 60688 01488b559910 parent 60526 fad653acf58f child 60804 080a979a985b
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:40 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:41 2015 +0200
1.3 @@ -44,7 +44,7 @@
1.4
1.5  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
1.6    apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
1.7 -  apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
1.8 +  apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
1.9    done
1.10
1.11  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
1.12 @@ -159,11 +159,11 @@
1.13
1.14
1.15  lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.16 -  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
1.17 +  by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat)
1.18
1.19  lemma prime_imp_power_coprime_int:
1.20    fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.21 -  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
1.22 +  by (metis coprime_exp_int gcd.commute prime_imp_coprime_int)
1.23
1.24  lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.25    by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
1.26 @@ -375,7 +375,7 @@
1.27  lemma bezout_gcd_nat:
1.28    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
1.29    using bezout_nat[of a b]