Def P  Q == PQ

is mentioned by

Thm* 'a,'b:S, x:'a+'b. isr(x)  inr(outr(x)) = x	[inr_houtr]
Thm* 'a,'b:S, x:'a+'b. isl(x)  inl(outl(x)) = x	[inl_houtl]
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, u,v:'a+'b. rep_sum(u) = rep_sum(v)  'a'b  u = v	[hrep_sum_inj]
Thm* 'a,'b:S, u:'a+'b. isr(u)  outr(u) = outr(u)	[houtr_nuprl]
Thm* 'a,'b:S, u:'a+'b. isl(u)  outl(u) = outl(u)	[houtl_nuprl]

In prior sections: core fun 1 well fnd int 1 bool 1 union hol hol bool

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