Def b == if b True else False fi

is mentioned by

Thm* P:(). P(0) & (n:. (m:. m<n  P(m))  P(n))  (n:. P(n))	[gen_induction]
Thm* P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))	[wop]
Thm* 'a:S, f:('a), x1,x2:'a. f(x1) & f(x2)  x1 = x2	[fun_eq_lemma]

In prior sections: bool 1 hol hol bool hol num hol prim rec hol arithmetic 2 hol min

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