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

is mentioned by

Thm* m,n:. ndiv(m;n)	[ndiv_wf]
Thm* m,n:. nmod(m;n)	[nmod_wf]
Thm* n:. n>0  odd(n) = odd(n-1)	[odd_pos]
Thm* n:. odd(n)	[odd_wf]
Thm* n:. n>0  even(n) = even(n-1)	[even_pos]
Thm* n:. even(n)	[even_wf]
Thm* n:. n>0  fact(n) = nfact(n-1)	[fact_pos]
Thm* n:. fact(n)	[fact_wf]
Thm* m,n:. n>0  exp(m;n) = mexp(m;n-1)	[exp_pos]
Thm* m:. exp(m;0) = 1	[exp_zero]
Thm* m,n:. exp(m;n)	[exp_wf]
Thm* m,n:. mn	[multiply_wf_nat]
Thm* m,n:. nnsub(m;n)	[nnsub_wf]
Thm* m,n:. mn  nnsub(n;m) = n-m	[nnsub_nuprl]
Thm* m,n:. m+n	[add_wf_nat]

In prior sections: core well fnd int 1 bool 1 fun 1 hol hol min hol bool

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