Def pq == if p q else false fi

is mentioned by

Thm* P1,P2:(T), L:T List. Thm* filter(P1;filter(P2;L)) ~ filter(t.(P1(t))(P2(t));L)

[filter_filter]

In prior sections: bool 1

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