Def ij == j<i

is mentioned by

Thm* i,j:. i<j  ji	[not_lt_int]
Thm* i,j:. ij  j<i	[not_le_int]

In prior sections: bool 1

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