Def True == 0  

is mentioned by

Thm* mt(nil) = True  Prop{1} Thm* & ('a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False  Prop{1})	[mt_def]
Def mt(l) == Case of l; nil  True ; a.as'  False	[mt]

In prior sections: core hol hol prim rec bool 1

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