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

is mentioned by

Thm* and Thm* (all(a:hnum. equal(abs_num(rep_num(a)),a)) Thm* ,all(r:hind. equal(is_num_rep(r),equal(rep_num(abs_num(r)),r))))	[hnum_iso_def]
Thm* exists(rep:hnum  hind. type_definition(is_num_rep,rep))	[hnum_ty_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* iso_pair(;;is_num_rep;rep_num;abs_num)	[num_iso]

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