Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
hanoi_PEGDef  Peg == {1...3}
Thm*  Peg  Type
int_isegDef  {i...j} == {k:ik & kj }
Thm*  i,j:. {i...j Type
le_intDef  ij == j<i
Thm*  i,j:. (ij 
natDef   == {i:| 0i }
Thm*    Type

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

Definitions HanoiTowers Sections NuprlLIB Doc