WhoCites Definitions hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites stype?
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}

Syntax:S has structure: stype

About:
setuniversemembertrueexists!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions hol sum Sections HOLlib Doc