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*  Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x)	[sfa_doc_alternate_zero_beyond]
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:A, x:A List. P(a.x)  R(a,x,P(x)))	[sfa_doc_listind_via_so]
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 X: A^n. P(u) Def == n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u))) Def (recursive)	[sfa_doc_ntuple_contains]
Def A =ext B == (X:A. X  B) & (X:B. X  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