src/HOL/Library/Primes.thy
changeset 21404 eb85850d3eb7
parent 21256 47195501ecf7
child 22665 cf152ff55d16
     1.1 --- a/src/HOL/Library/Primes.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/Primes.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -11,10 +11,11 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  coprime :: "nat => nat => bool"
     1.8 +  coprime :: "nat => nat => bool" where
     1.9    "coprime m n = (gcd (m, n) = 1)"
    1.10  
    1.11 -  prime :: "nat \<Rightarrow> bool"
    1.12 +definition
    1.13 +  prime :: "nat \<Rightarrow> bool" where
    1.14    "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    1.15  
    1.16