is mentioned by

Thm* it_sum(nil) = 0 Thm* & (l: List. mt(l)  it_sum(l) = head(l)+it_sum(tl(l))) Thm* & (x:, l: List. it_sum(cons(x; l)) = x+it_sum(l))	[it_sum_def]
Def it_sum == l: List. it_sum(l)	[hit_sum]

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