Def P  Q == P+Q

is mentioned by

Thm* p:. prime(p)  (a1,a2:. p | a1a2  p | a1  p | a2)	[prime_divs_prod]
Thm* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))	[prime_elim]
Thm* a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]
Thm* a,b:. GCD(a;0;b)  a = b  a = -b	[gcd_p_zero_rel]
Thm* a,b:. (a ~ b)  a = b  a = -b	[assoced_elim]
Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)	[prime]

In prior sections: core bool 1 int 2 rel 1

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