Def it_sum == l: List. it_sum(l)

is mentioned by

Thm* and Thm* (equal(it_sum(nil),0) Thm* ,all Thm* ,(h:hnum. all(t:hlist(hnum). equal(it_sum(cons(h,t)),add(h,it_sum(t))))))

[hit_sum_wd]

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