Def isl == u:'a+'b. isl(u)

is mentioned by

Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isl(x),equal(inl(outl(x)),x)))	[hinl_houtl]
Thm* 'a,'b:S. all(x:hsum('a; 'b). or(isl(x),isr(x)))	[hisl_or_isr]
Thm* 'b,'a:S. and(all(x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y)))))	[hisl_wd]

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