src/HOL/Number_Theory/Primes.thy
 changeset 44821 a92f65e174cf parent 40461 e876e95588ce child 44872 a98ef45122f3
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Sep 07 14:58:40 2011 +0200
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Sep 07 09:02:58 2011 -0700
1.3 @@ -174,7 +174,7 @@
1.4      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1.5    unfolding prime_int_altdef dvd_def
1.6    apply auto
1.7 -  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
1.8 +  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
1.9
1.10  lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
1.11      n > 0 --> (p dvd x^n --> p dvd x)"
1.12 @@ -220,7 +220,7 @@
1.13    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
1.14  proof
1.15    assume "?L" thus "?R"
1.16 -    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
1.17 +    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
1.18  next
1.19      assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
1.20  qed
1.21 @@ -272,7 +272,7 @@
1.22  lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.23    apply (rule prime_imp_coprime_int, assumption)
1.24    apply (unfold prime_int_altdef)
1.25 -  apply (metis int_one_le_iff_zero_less zless_le)
1.26 +  apply (metis int_one_le_iff_zero_less less_le)
1.27  done
1.28
1.29  lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
```