Def P  Q == P+Q

is mentioned by

Thm* x,y:. x<y & (z:. z<x  y<z)	[sfa_doc_simple_existential_2]
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))	[sfa_doc_or_dec]
Thm* A  B  (C:Prop. (A  C)  (B  C)  C)	[sfa_doc_or_via_so]
Thm* s:Sexpr(A). (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))	[sfa_doc_sexpr_case_thm]
Def a list xs == Case of xs; nil  False ; x.ys  x = a  A  a list ys Def (recursive)	[sfa_doc_inlist]
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]

In prior sections: core bool 1 rel 1 int 2 list 1 sqequal 1

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