Def P  Q == PQ

is mentioned by

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

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 hol hol bool hol num hol prim rec hol arithmetic 1 hol restr binder

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