--- a/src/ZF/ex/Primes.thy Thu Jun 13 14:25:45 1996 +0200
+++ b/src/ZF/ex/Primes.thy Thu Jun 13 16:22:37 1996 +0200
@@ -8,20 +8,20 @@
Primes = Arith +
consts
- dvd :: [i,i]=>o (infixl 70)
- gcd :: [i,i,i]=>o (* great common divisor *)
- egcd :: [i,i]=>i (* gcd by Euclid's algorithm *)
- coprime :: [i,i]=>o (* coprime definition *)
- prime :: [i]=>o (* prime definition *)
+ dvd :: [i,i]=>o (infixl 70)
+ gcd :: [i,i,i]=>o (* great common divisor *)
+ egcd :: [i,i]=>i (* gcd by Euclid's algorithm *)
+ coprime :: [i,i]=>o (* coprime definition *)
+ prime :: i=>o (* prime definition *)
defs
dvd_def "m dvd n == m:nat & n:nat & (EX k:nat. n = m#*k)"
- gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) \
-\ & (ALL d. (d dvd m) & (d dvd n) --> d dvd p)"
+ gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
+ (ALL d. (d dvd m) & (d dvd n) --> d dvd p)"
- egcd_def "egcd(m,n) == \
-\ transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m"
+ egcd_def "egcd(m,n) ==
+ transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m"
coprime_def "coprime(m,n) == egcd(m,n) = 1"