Def Dec(P) == P  P

is mentioned by

Thm* (P  Q)  (Dec(P)  Dec(Q))	[decidable_functionality]
Thm* Dec(A)  ((A & B)  A  B)	[not_over_and]
Thm* Dec(A)  (A  A)	[dneg_elim_a]
Thm* Dec(A)  A  A	[dneg_elim]
Thm* Dec(P)  SqStable(P)	[sq_stable_from_decidable]
Thm* Dec(P)  Stable{P}	[stable__from_decidable]
Thm* Dec(A)  (A  B)  Dec(B)	[iff_preserves_decidability]
Thm* a,b:Atom. Dec(a = b)	[decidable__atom_equal]
Thm* i,j:. Dec(i = j)	[decidable__int_equal]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__iff]
Thm* Dec(False)	[decidable__false]
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 XM == P:Prop. Dec(P)	[xmiddle]

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