src/HOL/Library/Primes.thy
changeset 28562 4e74209f113e
parent 27670 3b5425dead98
child 28952 15a4b2cf8c34
     1.1 --- a/src/HOL/Library/Primes.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  definition
     1.6    prime :: "nat \<Rightarrow> bool" where
     1.7 -  [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
     1.8 +  [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
     1.9  
    1.10  
    1.11  lemma two_is_prime: "prime 2"