Def  == Unit+Unit

is mentioned by

Thm* P:(). P(0) & (n:. P(n)  P(n+1))  (n:. P(n))	[induction]
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 hol min

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