Def (x:T. b(x))(x) == b(x)

is mentioned by

Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (and(P(0),all(n:hnum. implies(P(n),P(suc(n))))) Thm* (P:hnum  hbool. ,all(n:hnum. P(n))))	[hinduction]
Thm* all(m:hnum. all(n:hnum. implies(equal(suc(m),suc(n)),equal(m,n))))	[hinv_suc]
Thm* all(n:hnum. not(equal(suc(n),0)))	[hnot_suc]
Thm* all(m:hnum. equal(suc(m),abs_num(suc_rep(rep_num(m)))))	[hsuc_def]
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* equal(zero_rep,select(x:hind. all(y:hind. not(equal(x,suc_rep(y))))))	[hzero_rep_def]
Thm* equal(suc_rep,select(f:hind  hind. and(one_one(f),not(onto(f)))))	[hsuc_rep_def]
Def suc == n:. n+1	[hsuc]
Def abs_num == n:. @m:. (n = rep_num(m)  )	[habs_num]
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]
Def suc_rep == x:. (@f:. (one_one(;;f) & onto(;;f)))(x)	[hsuc_rep]

In prior sections: hol hol bool hol min

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