hol
one
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
v
:Unit.
v
=
[one_wd]
cites the following:
Thm*
all(
v
:hone. equal(
v
,one_el))
[hone_wd]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
one
Sections
HOLlib
Doc
v:Unit. v = 
v:hone. equal(v,one_el))v:Unit. v = v:hone. equal(v,one_el))