Def  P  Q == P+Q

is mentioned by

Thm*  X:. prime(X)  (a,b:. X | ab  X | a  X | b)	[nat_prime_div_each_factor]
Thm*  X:.  Thm*  prime(X) Thm*   Thm*  (X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)) Thm*   Thm*  (W:. 0<W  W<X  (t:. X | tW  X | t))	[nat_prime_div_each_factorLEMMA]

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

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