changeset 9548 | 15bee2731e43 |
parent 1793 | 09fff2f0d727 |
child 11316 | b4e71bd751e4 |
--- a/src/ZF/ex/Primes.thy Mon Aug 07 10:29:04 2000 +0200 +++ b/src/ZF/ex/Primes.thy Mon Aug 07 10:29:54 2000 +0200 @@ -6,7 +6,7 @@ The "divides" relation, the greatest common divisor and Euclid's algorithm *) -Primes = Arith + +Primes = Main + consts dvd :: [i,i]=>o (infixl 70) gcd :: [i,i,i]=>o (* great common divisor *)