Def (x:T. b(x))(x) == b(x)

is mentioned by

Def div == m:. n:. ndiv(m;n)	[hdiv]
Def mod == m:. n:. nmod(m;n)	[hmod]
Def odd == n:. odd(n)	[hodd]
Def even == n:. even(n)	[heven]
Def fact == n:. fact(n)	[hfact]
Def ge == m:. n:. nm	[hge]
Def le == m:. n:. mn	[hle]
Def gt == m:. n:. n<m	[hgt]
Def exp == m:. n:. exp(m;n)	[hexp]
Def mult == m:. n:. mn	[hmult]
Def sub == m:. n:. nnsub(m;n)	[hsub]
Def add == m:. n:. m+n	[hadd]

In prior sections: hol hol bool hol min

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