Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* n:, R:(nnProp), x,y:n. (x (R^*) y)  (k:(n+1). x R^k y)	[rel_star_finite]
Thm* R:(TTProp), k:, x,y:T. Thm* (x R^k y) Thm*  Thm* (L:T List.  Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))	[rel_exp_list]
Thm* L1,L:T List. interleaving(T;L1;nil;L)  L = L1	[nil_interleaving2]
Thm* L1,L:T List. interleaving(T;nil;L1;L)  L = L1	[nil_interleaving]
Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'. Thm* (x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))	[member_map_filter]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x)  (yL.P(y))	[l_exists_cons]
Thm* P:(TProp). (xnil.P(x))  False	[l_exists_nil]
Thm* l:T List, P:(T), x,y:T. Thm* x before y  filter(P;l)  P(x) & P(y) & x before y  l	[l_before_filter]
Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))	[sublist_filter]
Thm* L:T List, P:(T). (xL.P(x))  reduce(x,y. P(x)y;true;L)	[l_all_reduce]
Thm* f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x))  (xL.P(f(x)))	[l_all_map]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y))	[l_all_cons]

In prior sections: core well fnd int 1 bool 1 int 2 rel 1 num thy 1 fun 1 list 1 mb basic mb nat mb list 1

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