Def zero_rep == @x:. (y:. x = suc_rep(y)  )

is mentioned by

Thm* equal(0,abs_num(zero_rep))	[hzero_def]
Thm* all Thm* (m:hind. equal Thm* (m:hind. (is_num_rep(m) Thm* (m:hind. ,all Thm* (m:hind. ,(P:hind  hbool. implies Thm* (m:hind. ,(P:hind  hbool. (and Thm* (m:hind. ,(P:hind  hbool. ((P(zero_rep) Thm* (m:hind. ,(P:hind  hbool. (,all(n:hind. implies(P(n),P(suc_rep(n))))) Thm* (m:hind. ,(P:hind  hbool. ,P(m)))))	[his_num_rep_wd]
Thm* equal(zero_rep,select(x:hind. all(y:hind. not(equal(x,suc_rep(y))))))	[hzero_rep_def]
Def rep_num == n:. ncompose(suc_rep;n;zero_rep)	[hrep_num]
Def is_num_rep Def == m:. P: Def == m:. ((P(zero_rep))(n:. (P(n))(P(suc_rep(n)))))(P(m))	[his_num_rep]

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