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

is mentioned by

Thm* 'a,'b:S, x:'a+'b. isr(x)  inr(outr(x)) = x	[inr_houtr]
Thm* 'a,'b:S, x:'a+'b. isl(x)  isr(x)	[isl_or_isr]
Thm* 'a,'b:S, u:'a+'b. isr(u)  outr(u) = outr(u)	[houtr_nuprl]
Def isr == u:'a+'b. isr(u)	[hisr]

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