Def P  Q == P+Q

is mentioned by

Thm* P:(T), as:T List, d:T. Thm* ((first a  as s.t. P(a) else d)  as) Thm*  (first a  as s.t. P(a) else d) = d	[find_property]
Thm* l:T List, a,x,y:T. Thm* x before y  [a / l]  x = a & (y  l)  x before y  l	[cons_before]
Thm* x,y:T, L:T List. Thm* (x  L)  (y  L)  x = y  x before y  L  y before x  L	[l_tricotomy]
Thm* x1,x2:T, L1,L2:T List. Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2	[cons_sublist_cons]
Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2)	[member_append]
Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l)	[cons_member]

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

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