Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* n,k,r:. (q:. k = qn+r   & r<n)  nmod(k;n) = r	[mod_unique]
Thm* n,k,q:. (r:. k = qn+r   & r<n)  ndiv(k;n) = q	[ndiv_unique]
Thm* k,n:. 0<n  (r,q:. k = qn+r   & r<n)	[da]
Thm* P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))	[wop]
Thm* n,m:. n<m  (x:. n = x+m  )	[less_or_eq_add]
Thm* m,n:. n<m  (x:. m = n+x+1  )	[less_add_1]

In prior sections: core fun 1 hol hol bool hol prim rec int 2 hol arithmetic 3

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