Def  == Unit+Unit

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* P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)	[filter_iseg]
Thm* f:(T1T2), Q:(T2), L:T1 List. Thm* filter(Q;map(f;L)) = map(f;filter(Q o f;L))	[filter_map]
Thm* P:(T), l:T List. filter(P;l)  {x:T| P(x) } List	[filter_type]
Thm* P1,P2:(T), L:T List. Thm* filter(P1;filter(P2;L)) ~ filter(t.(P1(t))(P2(t));L)	[filter_filter]
Thm* P:(T), l1,l2:T List. filter(P;l1 @ l2) ~ (filter(P;l1) @ filter(P;l2))	[filter_append]
Thm* L:A List, f1,f2:(A). f1 = f2  (filter(f1;L) ~ filter(f2;L))	[filter_functionality]
Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)	[member_filter]

In prior sections: bool 1 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