Definitions hol arithmetic 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
expDef exp(m;n) == if n=0 then 1 else mexp(m;n-1) fi   (recursive)
Thm* m,n:. exp(m;n 
gtDef i>j == j<i
Thm* i,j:. (i>j Prop
natDef  == {i:| 0i }
Thm*   Type
Thm*   S

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

Definitions hol arithmetic 1 Sections HOLlib Doc