num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:A. B(x) == {x:A| B(x) }

is mentioned by

Thm* r:, s:{s':| CoPrime(r,s') }, a,b:.
Thm* x:. ((x = a mod r) & (x = b mod s))		[chrem_exists_a]
Thm* r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s))[chrem_exists_aux_a]
Thm* b:, a:. y:. GCD(a;b;y)[gcd_ex_n]

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

num thy 1 Sections StandardLIB Doc