Def  P & Q == PQ

is mentioned by

Thm*  a:.  Thm*  prime(a)  (p:, q:. pp = aqq  (p':. p'<p & qq = ap'p'))	[primes_sqr_roots_LEMMA1]
Thm*  p:, q:. pp = 2qq  (p':. p'<p & qq = 2p'p')	[two_sqr_roots_LEMMA1]
Thm*  P:(Prop). (x:. P(x)  (x':. x'<x & P(x')))  (x:. P(x))	[nat_descent]

In prior sections: core int 1 bool 1 LogicSupplement int 2 num thy 1 SimpleMulFacts rel 1

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