Def p  q == if p true else q fi

is mentioned by

Thm* b:. (false  b) = b	[bor_simp_4]
Thm* b:. (true  b) = true	[bor_simp_3]
Thm* b:. (b  false) = b	[bor_simp_2]
Thm* b:. (b  true) = true	[bor_simp_1]
Def or == p:. q:. p  q	[hor]

In prior sections: bool 1

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