Def P  Q == PQ

is mentioned by

Thm* a:T, Q:(TProp). (a = !x:T. Q(x))  a  {!x:T | Q(x)}	[uni_sat_imp_in_uni_set]
Thm* (P  Q)  (Q  P)  (P  Q)	[implies_antisymmetry]
Thm* (P  Q)  (P  Q)	[squash_functionality_wrt_iff]
Thm* (P  Q)  P  Q	[squash_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  P1  Q1  P2  Q2	[or_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  (P1  Q1  P2  Q2)	[or_functionality_wrt_iff]
Thm* (P  Q)  P  Q	[not_functionality_wrt_implies]
Thm* (P  Q)  (P  Q)	[not_functionality_wrt_iff]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  (x:S. P(x))  (y:T. Q(y))	[exists_functionality_wrt_implies]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[exists_functionality_wrt_iff]
Thm* P,Q:(SProp). Thm* S = T  (z:S. P(z)  Q(z))  (x:S. P(x))  (y:T. Q(y))	[all_functionality_wrt_implies]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[all_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2))	[iff_functionality_wrt_iff]
Thm* (P  Q)  (Dec(P)  Dec(Q))	[decidable_functionality]
Thm* (P1  P2)  (Q1  Q2)  (P1  Q1)  P2  Q2	[implies_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2))	[implies_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  P1 & Q1  P2 & Q2	[and_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  (P1 & Q1  P2 & Q2)	[and_functionality_wrt_iff]
Thm* (P  Q)  (Q  R)  P  R	[implies_transitivity]
Thm* (P  Q)  (Q  R)  (P  R)	[iff_transitivity]
Thm* Dec(A)  ((A & B)  A  B)	[not_over_and]
Thm* A  B  (A & B)	[not_over_and_b]
Thm* Dec(A)  (A  A)	[dneg_elim_a]
Thm* Dec(A)  A  A	[dneg_elim]
Thm* SqStable(P)  (P  P)	[squash_elim]
Thm* Dec(P)  SqStable(P)	[sq_stable_from_decidable]
Thm* Stable{P}  SqStable(P)	[sq_stable__from_stable]
Thm* P:(AProp). (x:A. SqStable(P(x)))  SqStable(x:A. P(x))	[sq_stable__all]
Thm* SqStable(P)  SqStable(Q)  SqStable(P  Q)	[sq_stable__iff]
Thm* SqStable(Q)  SqStable(P  Q)	[sq_stable__implies]
Thm* SqStable(P)  SqStable(Q)  SqStable(P & Q)	[sq_stable__and]
Thm* Dec(P)  Stable{P}	[stable__from_decidable]
Thm* f,g:(AB). (x:A. Stable{f(x) = g(x)})  Stable{f = g}	[stable__function_equal]
Thm* Dec(A)  (A  B)  Dec(B)	[iff_preserves_decidability]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__iff]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__implies]
Thm* Dec(P)  Dec(Q)  Dec(P & Q)	[decidable__and]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__or]
Def a = !x:T. Q(x) == Q(a) & (a':T. Q(a')  a' = a)	[uni_sat]
Def {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y)  y = x) }	[unique_set]
Def SqStable(P) == P  P	[sq_stable]
Def Stable{P} == P  P	[stable]
Def P  Q == (P  Q) & (P  Q)	[iff]
Def A == A  False	[not]
Def P  Q == Q  P	[rev_implies]

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