Def onto == f:'a'b. onto('a;'b;f)

is mentioned by

Thm* exists(f:hind  hind. and(one_one(f),not(onto(f))))	[hinfinity_ax]
Thm* 'a,'b:S. Thm* all(f:'a  'b. equal(onto(f),all(y:'b. exists(x:'a. equal(y,f(x))))))	[honto_def]

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