Def True == 0  

is mentioned by

Thm* A  True  True	[or_true_r]
Thm* True  A  True	[or_true_l]
Thm* A & True  A	[and_true_r]
Thm* True & A  A	[and_true_l]
Def T == {:True| T }	[squash]

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