Def pq == if p q else false fi

is mentioned by

Thm* b:. (bfalse) = false	[band_simp_2]
Thm* b:. (trueb) = b	[band_simp_3]
Thm* b:. (falseb) = false	[band_simp_4]
Thm* b:. (btrue) = b	[band_simp_1]
Def and == p:. q:. pq	[hand]
Def b_exists_unique('a;x.p(x)) Def == (x:'a. p(x))(x,y:'a.  (p(x)p(y))(x = y))	[b_exists_unique]

In prior sections: bool 1 hol

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