is mentioned by

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

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