Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)

is mentioned by

Thm* p:. prime(p)  (a1,a2:. p | a1a2  p | a1  p | a2)	[prime_divs_prod]
Thm* a:. atomic(a)  prime(a)	[atomic_imp_prime]
Thm* a,p:. prime(p)  (CoPrime(p,a)  p | a)	[coprime_iff_ndivides]
Thm* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))	[prime_elim]
Thm* a:. prime(a)  atomic(a)	[prime_imp_atomic]

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