Def |i| == if 0i i else -i fi

is mentioned by

Thm* a:. |a| ~ a	[absval_assoced]
Thm* a,b:. |a| | |b|  a | b	[divides_of_absvals]

In prior sections: int 2

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