Def isl(x) == InjCase(x; y. true; z. false)

is mentioned by

Thm* 'a,'b:S, x:'a+'b. isl(x)  inl(outl(x)) = x	[inl_houtl]
Thm* 'a,'b:S, x:'a+'b. isl(x)  isr(x)	[isl_or_isr]
Thm* 'a,'b:S, u:'a+'b. isl(u)  outl(u) = outl(u)	[houtl_nuprl]
Def isl == u:'a+'b. isl(u)	[hisl]

In prior sections: union

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