Def mult == m:. n:. mn

is mentioned by

Thm* all Thm* (k:hnum. all Thm* (k:hnum. (n:hnum. implies Thm* (k:hnum. (n:hnum. (lt(0,n) Thm* (k:hnum. (n:hnum. ,exists Thm* (k:hnum. (n:hnum. ,(r:hnum. exists Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. and Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. (equal(k,add(mult(q,n),r)) Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. ,lt(r,n)))))))	[hda]
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. (m:hnum. all Thm* (p:hnum. (m:hnum. (n:hnum. equal Thm* (p:hnum. (m:hnum. (n:hnum. (equal(mult(n,suc(p)),mult(m,suc(p))) Thm* (p:hnum. (m:hnum. (n:hnum. ,equal(n,m)))))	[hmult_suc_eq]
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* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(p,sub(m,n)) Thm* (m:hnum. (n:hnum. (p:hnum. ,sub(mult(p,m),mult(p,n))))))	[hleft_sub_distrib]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(sub(m,n),p) Thm* (m:hnum. (n:hnum. (p:hnum. ,sub(mult(m,p),mult(n,p))))))	[hright_sub_distrib]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. implies(le(m,n),le(mult(m,p),mult(n,p))))))	[hless_mono_mult]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal(mult(m,mult(n,p)),mult(mult(m,n),p)))))	[hmult_assoc]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(p,add(m,n)) Thm* (m:hnum. (n:hnum. (p:hnum. ,add(mult(p,m),mult(p,n))))))	[hleft_add_distrib]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(add(m,n),p) Thm* (m:hnum. (n:hnum. (p:hnum. ,add(mult(m,p),mult(n,p))))))	[hright_add_distrib]
Thm* all(m:hnum. all(n:hnum. equal(mult(m,n),mult(n,m))))	[hmult_sym]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. and Thm* (m:hnum. (n:hnum. (equal(mult(0,m),0) Thm* (m:hnum. (n:hnum. ,and Thm* (m:hnum. (n:hnum. ,(equal(mult(m,0),0) Thm* (m:hnum. (n:hnum. ,,and Thm* (m:hnum. (n:hnum. ,,(equal(mult(1,m),m) Thm* (m:hnum. (n:hnum. ,,,and Thm* (m:hnum. (n:hnum. ,,,(equal(mult(m,1),m) Thm* (m:hnum. (n:hnum. ,,,,and Thm* (m:hnum. (n:hnum. ,,,,(equal(mult(suc(m),n),add(mult(m,n),n)) Thm* (m:hnum. (n:hnum. ,,,,,equal(mult(m,suc(n)),add(m,mult(m,n))))))))))	[hmult_clauses]
Thm* all(m:hnum. equal(mult(m,1),m))	[hmult_right_1]
Thm* all(m:hnum. equal(mult(1,m),m))	[hmult_left_1]
Thm* all(m:hnum. all(n:hnum. equal(mult(m,suc(n)),add(m,mult(m,n)))))	[hmult_suc]
Thm* all(m:hnum. equal(mult(m,0),0))	[hmult_0]
Thm* all Thm* (n:hnum. implies Thm* (n:hnum. (lt(0,n) Thm* (n:hnum. ,all Thm* (n:hnum. ,(k:hnum. and Thm* (n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n))) Thm* (n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))	[hdivision]
Thm* and Thm* (equal(fact(0),1) Thm* ,all(n:hnum. equal(fact(suc(n)),mult(suc(n),fact(n)))))	[hfact_wd]
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]
Thm* and Thm* (all(n:hnum. equal(mult(0,n),0)) Thm* ,all(m:hnum. all(n:hnum. equal(mult(suc(m),n),add(mult(m,n),n)))))	[hmult_wd]

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