Def  P & Q == PQ

is mentioned by

Thm*  R:(AAProp).  Thm*  (EquivRel x,y:A. R(x,y)) Thm*   Thm*  (x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z))))	[equivrel_characterization]
Thm*  {x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) }	[exteq_subset_vs_and]
Thm*  P XOR Q  (Q  P) & Dec(P)	[xor_vs_neg_n_dec]
Def  x is the u:A. P(u) == P(x) & (u:A. P(u)  u = x)	[is_the]
Def  P XOR Q == P  Q & (P & Q)	[xor]
Def  A =ext B == (x:A. x  B) & (x:B. x  A)	[exteq]

In prior sections: core int 1 bool 1 rel 1

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