NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def P & Q == PQ

is mentioned by

Thm* x:y:yyx & x<(y+1)(y+1)[sfa_doc_nat_sqrt]
Thm* x,y:x<y & (z:z<x  y<z)[sfa_doc_simple_existential_2]
Thm* f,g:().
Thm* (x:f zero beyond x) & (x:g zero beyond x)
Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x)
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))[sfa_doc_or_dec]
Thm* R:(A(A List)PropProp). 
Thm* P:((A List)Prop). 
Thm* (P(nil)  Q) & (a:Ax:A List. P(a.x R(a,x,P(x)))
Thm* A & B  (C:Prop. (A  B  C C)[sfa_doc_and_via_so]
Thm* A:Prop, B:Prop(given A). (A & B Prop[sfa_doc_and_typing]
Thm* k:. 0<k & (2  k)<1  2<k[sfa_doc_cand_example]
Def Induction for x:P(x) == P(0) & (x:P(x P(x+1))  (x:P(x))[sfa_doc_indscheme]
Def  u in XA^nP(u)
Def == n = 1   & P(X n2 & (X/a,restP(a ( u in restA^(n-1). P(u)))
Def (recursive)
Def A =ext B == (X:AX  B) & (X:BX  A)[sfa_doc_exteq]

In prior sections: core int 1 bool 1 int 2 rel 1 fun 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

NuprlPrimitives Sections NuprlLIB Doc