hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
i
,
j
:
.
i
j
j
<
i
[not_le_int]
cites the following:
1
Thm*
i
,
j
:
.
i
j
= (
j
<
i
)
[bnot_of_le_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:. ij = (j<i)i,j:. ij j<ii,j:. ij = (j<i)