Definitions hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
it_sumDef it_sum(l) == if null(l) then 0 else head(l)+it_sum(tl(l)) fi   (recursive)
Thm* l: List. it_sum(l 
natDef  == {i:| 0i }
Thm*   Type
Thm*   S

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

Definitions hol list 1 Sections HOLlib Doc