Def  P XOR Q == P  Q & (P & Q)

is mentioned by

Thm*  P XOR Q  (Q  P) & Dec(P)

[xor_vs_neg_n_dec]

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