Def pq == if p q else false fi

is mentioned by

Def is_num_rep Def == m:. P: Def == m:. ((P(zero_rep))(n:. (P(n))(P(suc_rep(n)))))(P(m))

[his_num_rep]

In prior sections: bool 1 hol hol bool

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