Def b == if b false else true fi

is mentioned by

Thm* false = true	[bnot_simp_2]
Thm* true = false	[bnot_simp_1]
Def not == p:. p	[hnot]

In prior sections: bool 1 hol

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