Def P & Q == PQ

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]
Thm* mt(nil) = True  Prop{1} Thm* & ('a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False  Prop{1})	[mt_def]
Thm* l,ll:'a List. mt(l @ ll)  mt(l) & mt(ll)	[mt_append]

In prior sections: core int 1 bool 1 int 2 hol hol bool hol num hol pair hol prim rec fun 1 hol restr binder

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