hol one Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* 'a:S, f,g:('aUnit). f = g[one_axiom]
cites the following:
Thm* 'a:S. all(f:'a  hone. all(g:'a  hone. equal(f,g)))[hone_axiom]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol one Sections HOLlib Doc