Def atomic(a) == a = 0 & (a ~ 1) & reducible(a)

is mentioned by

Thm* a:. atomic(a)  prime(a)	[atomic_imp_prime]
Thm* a:. prime(a)  atomic(a)	[prime_imp_atomic]
Thm* a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]

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