Def flat == l:('a List) List. flatten(l)

is mentioned by

Thm* 'a:S.  Thm* and Thm* (equal(flat(nil),nil) Thm* ,all Thm* ,(h:hlist('a). all Thm* ,(h:hlist('a). (t:hlist(hlist('a)). equal Thm* ,(h:hlist('a). (t:hlist(hlist('a)). (flat(cons(h,t)) Thm* ,(h:hlist('a). (t:hlist(hlist('a)). ,append(h,flat(t))))))

[hflat_wd]

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