is mentioned by

Thm* 'b,'a:S, x:('a  'b). Thm* (x:'b. x) o x = x  ('a  'b) & x o (x:'a. x) = x  ('a  'b)	[i_o_id]
Thm* 'a,'c,'d,'b:S, x:('c  'd), x@0:('b  'c), x@1:('a  'b). Thm* x o (x@0 o x@1) = (x o x@0) o x@1  ('a  'd)	[o_assoc]
Thm* 'b,'c,'a:S, x:('b  'c), x@0:('a  'b), x@1:'a. Thm* (x o x@0)(x@1) = x(x@0(x@1))	[o_thm]
Def o == f:'a'b. g:'a'b. f o g	[ho]

In prior sections: fun 1

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