IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
qmul dist over qadd11 1. a : 2. b : 3. c : a *q b +q c.numa *q b +q a *q c.den = a *q b +q a *q c.numa *q b +q c.den
By:
OnHyps [3;2;1] RatHD THEN Unfolds [`qadd`;`qmul`] 0 THEN RW (DepthC qnd_evalC) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a *q b +q c.num
a *q b +q a *q c.den = a *q b +q a *q c.num
