Def not == p:. p

is mentioned by

Thm* exists(f:hind  hind. and(one_one(f),not(onto(f))))	[hinfinity_ax]
Thm* equal(not,t:hbool. implies(t,f))	[hnot_def]

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