Def or == p:. q:. p  q

is mentioned by

Thm* 'a:S.  Thm* all Thm* (l:hlist('a). or Thm* (l:hlist('a). (equal(l,nil) Thm* (l:hlist('a). ,exists(t:hlist('a). exists(h:'a. equal(l,cons(h,t))))))

[hlist_cases]

In prior sections: hol bool hol prim rec

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