Def t == true

is mentioned by

Thm* 'a:S.  Thm* and Thm* (all(P:'a  hbool. equal(every(P,nil),t)) Thm* ,all Thm* ,(P:'a  hbool. all Thm* ,(P:'a  hbool. (h:'a. all Thm* ,(P:'a  hbool. (h:'a. (t:hlist('a). equal Thm* ,(P:'a  hbool. (h:'a. (t:hlist('a). (every(P,cons(h,t)) Thm* ,(P:'a  hbool. (h:'a. (t:hlist('a). ,and(P(h),every(P,t)))))))	[hevery_def]
Thm* 'a:S.  Thm* and Thm* (equal(null(nil),t) Thm* ,all(t:hlist('a). all(h:'a. equal(null(cons(h,t)),f))))	[hnull_def]

In prior sections: hol bool hol restr binder hol list 1

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