hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* 0<0+1[less_0_0]
cites the following:
Thm* lt(0,suc(0))[hless_0_0]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol prim rec Sections HOLlib Doc