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)"