Def True == 0  

is mentioned by

Thm* t:A. t = t  True	[eq_refl]
Thm* False  True	[not_false]
Thm* True  False	[not_true]
Thm* x:A. (y:A. x = y)  True	[exists_explicit_2]
Thm* x:A. (y:A. y = x)  True	[exists_explicit_1]
Thm* (x:A. True)  True	[all_true]
Thm* (True  P)  P	[true_imp]
Thm* (False  P)  True	[false_imp]
Thm* (P  True)  True	[imp_true]
Thm* P & True  P	[and_true]
Thm* True  P  True	[true_or]
Thm* P  True  True	[or_true]
Thm* True & P  P	[true_and]
Thm* true  True	[assert_of_btrue]
Thm* 'a:S, P:('aProp). lem('a) = lem({x:'a| True })  'a	[lem_extensionality_axiom]
Def S == {T:Type| x:T. True }	[stype]

In prior sections: core bool 1

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