src/HOL/Library/Primes.thy
changeset 27106 ff27dc6e7d05
parent 26757 e775accff967
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/Primes.thy	Tue Jun 10 15:30:54 2008 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Tue Jun 10 15:30:56 2008 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Library/Primes.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Amine Chaieb Christophe Tabacznyj and Lawrence C Paulson
     1.7 +    Author:     Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
     1.8      Copyright   1996  University of Cambridge
     1.9  *)
    1.10  
    1.11 @@ -16,7 +16,7 @@
    1.12  
    1.13  definition
    1.14    prime :: "nat \<Rightarrow> bool" where
    1.15 -  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    1.16 +  [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    1.17  
    1.18  
    1.19  lemma two_is_prime: "prime 2"