hol combin Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* 'a:S, x:'ax = x[i_thm]
cites the following:
Thm* 'a:S. all(x:'a. equal(i(x),x))[hi_thm]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol combin Sections HOLlib Doc