Def Y(f) == (x.f(x(x)))(x.f(x(x)))

is mentioned by

Def odd(n) == if n=0 then false else odd(n-1) fi   (recursive)	[odd]
Def even(n) == if n=0 then true else even(n-1) fi   (recursive)	[even]
Def fact(n) == if n=0 then 1 else nfact(n-1) fi   (recursive)	[fact]
Def exp(m;n) == if n=0 then 1 else mexp(m;n-1) fi   (recursive)	[exp]

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