Definitions num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
assocedDef a ~ b == a | b & b | a
Thm* a,b:. (a ~ b Prop
equiv_relDef EquivRel x,y:TE(x;y)
Def == Refl(T;x,y.E(x;y)) & (Sym x,y:TE(x;y)) & (Trans x,y:TE(x;y))
Thm* T:Type, E:(TTProp). (EquivRel x,y:TE(x,y))  Prop
iffDef P  Q == (P  Q) & (P  Q)
Thm* A,B:Prop. (A  B Prop

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

Definitions num thy 1 Sections StandardLIB Doc