Def b == if b True else False fi

is mentioned by

Thm* k:, P:(k). Thm* ((i:k. P(i))  0<search(k;P)) Thm* & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))

[search_property]

In prior sections: bool 1 list 1 rel 1

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