# HG changeset patch
# User paulson
# Date 864998629 -7200
# Node ID 0cc2eaa8b0f9ecb3cb60dcb452ae2caaff48fcb7
# Parent  d9b30c300f1e7cb361c6c24cafc2ac54bf62f8c4
Now "primes" is a set

diff -r d9b30c300f1e -r 0cc2eaa8b0f9 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Fri May 30 15:23:25 1997 +0200
+++ b/src/HOL/ex/Primes.thy	Fri May 30 15:23:49 1997 +0200
@@ -3,28 +3,25 @@
     Author:     Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 
-The "divides" relation, the Greatest Common Divisor and Euclid's algorithm
+The Greatest Common Divisor and Euclid's algorithm
 *)
 
-Primes = Arith + WF_Rel +
+Primes = Divides + WF_Rel +
 consts
-  dvd     :: [nat,nat]=>bool              (infixl 70) 
   is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
   gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
   coprime :: [nat,nat]=>bool
-  prime   :: nat=>bool
+  prime   :: nat set
   
 recdef gcd "measure ((%(x,y).y) ::nat*nat=>nat)"
     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
 
 defs
-  dvd_def     "m dvd n == EX k. n = m*k"
-
   is_gcd_def  "is_gcd p m n == p dvd m  &  p dvd n  &
                                (ALL d. d dvd m & d dvd n --> d dvd p)"
 
   coprime_def "coprime m n == gcd(m,n) = 1"
 
-  prime_def   "prime(n) == (1<n) & (ALL m. 1<m & m<n --> ~(m dvd n))"
+  prime_def   "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
 
 end