Def let == f:'a'b. e:'a. let x = e in f(x)

is mentioned by

Thm* 'b,'a:S. equal(let,f:'a  'b. x:'a. f(x))

[hlet_def]

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