Def or == p:. q:. p  q

is mentioned by

Thm* all(t:hbool. or(equal(t,t),equal(t,f)))	[hbool_cases_ax]
Thm* equal Thm* (or Thm* ,t1:hbool. t2:hbool. all Thm* ,t1:hbool. t2:hbool. (t:hbool. implies Thm* ,t1:hbool. t2:hbool. (t:hbool. (implies(t1,t) Thm* ,t1:hbool. t2:hbool. (t:hbool. ,implies(implies(t2,t),t))))	[hor_def]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html