Def i<j == if i<j true ; false fi

is mentioned by

Thm* x,y:. x<y  x<y	[assert_of_lt_int]
Thm* i,j:. ij = (j<i)	[bnot_of_le_int]
Def ij == j<i	[le_int]

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