Definitions hol arithmetic 3 HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Defined Operators mentioned in hol arithmetic 3

DefA[not]core
Defx:A. B(x)[all]core
DefP & Q[and]core
Defx:A. B(x)[exists]core
DefP  Q[or]core
DefP  Q[implies]core
DefP  Q[iff]core
DefP  Q[rev_implies]core

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

Definitions hol arithmetic 3 HOLlib Doc