src/ZF/ex/Primes.thy
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 *)