Def imax(a;b) == if ab b else a fi

is mentioned by

Thm* a,b:. (a -- b)+b = imax(a;b)	[ndiff_add_eq_imax]
Thm* a,b:. imax(a;b) = imax(b;a)	[imax_com]
Thm* a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)	[imax_assoc]
Thm* a,b,c:. imax(a;b)+c = imax(a+c;b+c)	[imax_add_r]
Thm* a,b,c:. aimax(b;c)  ab  ac	[imax_ub]
Thm* a,b,c:. imax(a;b)c  ac & bc	[imax_lb]
Thm* a,b:. -imin(a;b) = imax(-a;-b)	[minus_imin]
Thm* a,b:. -imax(a;b) = imin(-a;-b)	[minus_imax]
Def a -- b == imax(a-b;0)	[ndiff]

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