Def P & Q == PQ

is mentioned by

Thm* n,m:. Thm* 0+m = m   & m+0 = m   & m+1+n = m+n+1   & m+(n+1) = (m+n)+1

[add_clauses]

In prior sections: core

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