Def P  Q == PQ

is mentioned by

Thm* p,q,r,s:. p =q q  r =q s  p *q r =q q *q s	[qmul_functionality]
Thm* p,q,r,s:. p =q q  r =q s  p +q r =q q +q s	[qadd_functionality]
Thm* x,y,z:. x =q y  y =q z  x =q z	[eq_rat_trans]
Thm* x,y:. x =q y  y =q x	[eq_rat_sym]

In prior sections: core well fnd int 1 bool 1 int 2

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