WhoCites Definitions hol sum Sections HOLlib Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites hsum?
hsumDef hsum('a'b) == 'a+'b
Thm* 'a,'b:S. hsum('a'b S

About:
unionmemberall!abstraction
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions hol sum Sections HOLlib Search Doc