Def gcd(a;b) == if b=0 a else gcd(b;a rem b) fi  (recursive)

is mentioned by

Thm* a,b:. CoPrime(a,b)  (gcd(a;b) ~ 1)	[coprime_elim_a]
Thm* a,b,c:. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))	[gcd_assoc]
Thm* a,b,n:. (ngcd(a;b)) ~ gcd(na;nb)	[gcd_mul]
Thm* a,b,c:. c | a  c | b  c | gcd(a;b)	[gcd_is_gcd]
Thm* a,b:. gcd(a;b) | b	[gcd_is_divisor_2]
Thm* a,b:. gcd(a;b) | a	[gcd_is_divisor_1]
Thm* a,b:. gcd(a;b) ~ gcd(b;a)	[gcd_sym]
Thm* a,b:. y:. GCD(a;b;y) & gcd(a;b) = y	[gcd_elim]
Thm* a,b:. GCD(a;b;gcd(a;b))	[gcd_sat_pred]
Thm* a,b:. GCD(a;b;gcd(a;b))	[gcd_sat_gcd_p]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html