Def pq == if p q else false fi

is mentioned by

Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l)  every(P;l) & every(Q;l)	[every_conj]
Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))	[every_conj_2]

In prior sections: bool 1 hol hol bool hol num hol pair hol list 1

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