hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
i
,
j
:
.
i
<
j
j
i
[not_lt_int]
cites the following:
Thm*
i
,
j
:
.
i
<
j
= (
j
i
)
[bnot_of_lt_int]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
Sections
HOLlib
Doc
i,j:
. 
i<
j 
j
ii,j:. i<j = (ji)i,j:. i<j jii,j:. i<j = (ji)