Def abs_num == n:. @m:. (n = rep_num(m)  )

is mentioned

In prior sections: hol num

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html