Def o == f:'a'b. g:'a'b. f o g

is mentioned by

Thm* 'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f)))	[hi_o_id]
Thm* 'a,'c,'d,'b:S. Thm* all Thm* (f:'c  'd. all Thm* (f:'c  'd. (g:'b  'c. all Thm* (f:'c  'd. (g:'b  'c. (h:'a  'b. equal(o(f,o(g,h)),o(o(f,g),h)))))	[ho_assoc]
Thm* 'b,'c,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. all(x:'a. equal(o(f,g,x),f(g(x))))))	[ho_thm]
Thm* 'c,'b,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. equal(o(f,g),x:'a. f(g(x)))))	[ho_def]

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