Def select == p:'a. @x:'a. (p(x))

is mentioned by

Thm* equal(one_el,select(x:hone. t))

[hone_def]

In prior sections: hol bool

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