Def x:A. B(x) == x:AB(x)

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]

In prior sections: core fun 1 hol hol bool

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