Def inr == x:'b. inr(x)

is mentioned by

Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isr(x),equal(inr(outr(x)),x)))	[hinr_houtr]
Thm* 'c,'b,'a:S. Thm* all Thm* (f:'a  'c. all Thm* (f:'a  'c. (g:'b  'c. exists_unique Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (all Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. equal Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. (h(inl(x)) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. ,f(x))) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,all Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. equal Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. (h(inr(x)) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. ,g(x)))))))	[hsum_axiom_2]
Thm* 'c,'b,'a:S. Thm* all Thm* (f:'a  'c. all Thm* (f:'a  'c. (g:'b  'c. exists_unique Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (equal(o(h,inl),f) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,equal(o(h,inr),g)))))	[hsum_axiom]
Thm* 'b,'a:S. all(x:'b. equal(outr(inr(x)),x))	[houtr_wd]
Thm* 'a,'b:S. and(all(x:'b. isr(inr(x))),all(y:'a. not(isr(inl(y)))))	[hisr_wd]
Thm* 'b,'a:S. and(all(x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y)))))	[hisl_wd]
Thm* 'a,'b:S. Thm* all Thm* (e:'b. equal Thm* (e:'b. (inr(e) Thm* (e:'b. ,abs_sum(b:hbool. x:'a. y:'b. and(equal(y,e),not(b)))))	[hinr_def]

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