Def exp == m:. n:. exp(m;n)

is mentioned by

Thm* all Thm* (p:hnum. all Thm* (p:hnum. (q:hnum. all Thm* (p:hnum. (q:hnum. (n:hnum. all Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. equal Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. (equal Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. ((mult(n,exp(suc(q),p)) Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. (,mult(m,exp(suc(q),p))) Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. ,equal(n,m))))))	[hmult_exp_mono]
Thm* all Thm* (p:hnum. all Thm* (p:hnum. (q:hnum. all Thm* (p:hnum. (q:hnum. (n:hnum. equal Thm* (p:hnum. (q:hnum. (n:hnum. (exp(n,add(p,q)) Thm* (p:hnum. (q:hnum. (n:hnum. ,mult(exp(n,p),exp(n,q))))))	[hexp_add]
Thm* and Thm* (all(m:hnum. equal(exp(m,0),1)) Thm* ,all(m:hnum. all(n:hnum. equal(exp(m,suc(n)),mult(m,exp(m,n))))))	[hexp_wd]

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