src/HOL/GCD.thy
changeset 32111 7c39fcfffd61
parent 32045 efc5f4806cd5
child 32112 6da9c2a49fed
     1.1 --- a/src/HOL/GCD.thy	Mon Jul 20 20:03:19 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Tue Jul 21 11:01:07 2009 +0200
     1.3 @@ -1657,6 +1657,20 @@
     1.4  lemma two_is_prime_int [simp]: "prime (2::int)"
     1.5  by simp
     1.6  
     1.7 +text{* A bit of regression testing: *}
     1.8 +
     1.9 +lemma "prime(97::nat)"
    1.10 +by simp
    1.11 +
    1.12 +lemma "prime(97::int)"
    1.13 +by simp
    1.14 +
    1.15 +lemma "prime(997::nat)"
    1.16 +by eval
    1.17 +
    1.18 +lemma "prime(997::int)"
    1.19 +by eval
    1.20 +
    1.21  
    1.22  lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
    1.23    apply (rule coprime_exp_nat)