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

is mentioned by

Thm* m,n:. n<m  (x:. x+n = m  )	[less_add]
Thm* m:. m = 0    (n:. m = n+1  )	[num_cases]

In prior sections: core

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