Def abs_list == r:('a). @a:'a List. (r = rep_list('a;a))

is mentioned by

Thm* 'a:S. equal(nil,abs_list(pair((n:hnum. select(e:'a. t)),0)))	[hnil_def]
Thm* 'a:S.  Thm* and Thm* (all(a:hlist('a). equal(abs_list(rep_list(a)),a)) Thm* ,all Thm* ,(r:hprod((hnum  'a); hnum). equal Thm* ,(r:hprod((hnum  'a); hnum). (is_list_rep(r) Thm* ,(r:hprod((hnum  'a); hnum). ,equal(rep_list(abs_list(r)),r))))	[hlist_iso_def]
Thm* 'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	[list_iso]

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