Def P & Q == PQ

is mentioned by

Thm* 'c,'b,'a:S, f:('a'c), g:('b'c). Thm* (h:(('a+'b)'c). (x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x))) Thm* & (h,y:(('a+'b)'c). Thm* & ((x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x)) Thm* & (& (x:'a. y(inl(x)) = f(x)) Thm* & (& (x:'b. y(inr(x)) = g(x)) Thm* & ( Thm* & (h = y)	[sum_axiom_2]
Thm* 'c,'b,'a:S, f:('a'c), g:('b'c). Thm* (h:(('a+'b)'c).  Thm* (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c) Thm* & (h,y:(('a+'b)'c). Thm* & (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c Thm* & (& y o (x:'a. inl(x)) = f  'a'c Thm* & (& y o (x:'b. inr(x)) = g  'b'c Thm* & ( Thm* & (h = y)	[sum_axiom]
Thm* 'a,'b:S. Thm* (x:'a+'b. abs_sum(rep_sum(x)) = x  'a+'b) Thm* & (x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x))	[sum_iso]

In prior sections: core int 1 bool 1 hol hol bool hol combin fun 1

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