Def P  Q == P+Q

is mentioned by

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* A  True  True	[or_true_r]
Thm* True  A  True	[or_true_l]
Thm* A  False  A	[or_false_r]
Thm* False  A  A	[or_false_l]
Thm* Dec(A)  ((A & B)  A  B)	[not_over_and]
Thm* A  B  (A & B)	[not_over_and_b]
Thm* (A  B)  A & B	[not_over_or_a]
Thm* (A  B)  A & B	[not_over_or]
Thm* A  B  B  A	[or_comm]
Thm* A  (B  C)  (A  B)  C	[or_assoc]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__or]
Def Dec(P) == P  P	[decidable]

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