Def  == Unit+Unit

is mentioned by

Thm* 'a:Type, p:('a), l:'a List. every(p;l)	[every_wf]
Def every == p:'a. l:'a List. every(p;l)	[hevery]

In prior sections: bool 1 list 1 hol hol bool hol num hol arithmetic 1 hol min hol restr binder hol pair

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