Def t == true

is mentioned by

Thm* all(t:hbool. or(equal(t,t),equal(t,f)))	[hbool_cases_ax]
Thm* 'a:S.  Thm* equal Thm* (cond Thm* ,t:hbool. t1:'a. t2:'a. select Thm* ,t:hbool. t1:'a. t2:'a. (x:'a. and Thm* ,t:hbool. t1:'a. t2:'a. (x:'a. (implies(equal(t,t),equal(x,t1)) Thm* ,t:hbool. t1:'a. t2:'a. (x:'a. ,implies(equal(t,f),equal(x,t2)))))	[hcond_def]
Thm* 'a:S. equal(all,P:'a  hbool. equal(P,x:'a. t))	[hforall_def]
Thm* equal(t,equal((x:hbool. x),x:hbool. x))	[htruth]

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