Def  P  Q == P+Q

is mentioned by

Thm*  a,b:. prime(ab)  ab = a  ab = b	[prime_among_factors]
Thm*  x:. prime(x)  x<2  (i,j:{2..x}. x = ij)	[nonprime_nat]
Thm*  a,b:. ab = 0  a = 0  b = 0	[prod_zero_iff_factor_zero]

In prior sections: core bool 1 rel 1 LogicSupplement int 2 num thy 1

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