Def  P  Q == P+Q

is mentioned by

Thm*  x,a:A, ys:A List. (x  a.ys)  x = a  (x  ys)	[is_list_mem_split]
Def  a  xs == Case of xs; nil  False ; x.ys  a = x  A  (a  ys) Def  (recursive)	[is_list_mem]

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

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