hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def A == A  False

is mentioned by

Thm* 'a:S, l:'a List. mt(l hd(l) = head(l)[hhd_nuprl]
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(xl)) = x+it_sum(l))
[it_sum_def]
Thm* 'a:Type, l:'a List. mt(l head(l 'a[head_wf]

In prior sections: core bool 1 int 2 list 1 hol hol bool hol num hol prim rec

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

hol list 1 Sections HOLlib Doc