Def a *q b == (a.numb.num)/(a.denb.den)

is mentioned by

Thm* a,b,c:. a *q b +q c =q a *q b +q a *q c	[qmul_dist_over_qadd]
Thm* p,q:. p *q q =q q *q p	[qmul_com]
Thm* p,q,r:. p *q q *q r =q p *q q *q r	[qmul_assoc]
Thm* p,q,r,s:. p =q q  r =q s  p *q r =q q *q s	[qmul_functionality]

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