Def not == p:. p

is mentioned by

Thm* 'a,'b:S. and(all(x:'b. isr(inr(x))),all(y:'a. not(isr(inl(y)))))	[hisr_wd]
Thm* 'b,'a:S. and(all(x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y)))))	[hisl_wd]
Thm* 'a,'b:S. Thm* all Thm* (e:'b. equal Thm* (e:'b. (inr(e) Thm* (e:'b. ,abs_sum(b:hbool. x:'a. y:'b. and(equal(y,e),not(b)))))	[hinr_def]
Thm* 'a,'b:S. Thm* all Thm* (f:hbool Thm* ( 'a Thm* ( 'b Thm* ( hbool. equal Thm* ( hbool. (is_sum_rep(f) Thm* ( hbool. ,exists Thm* ( hbool. ,(v1:'a. exists Thm* ( hbool. ,(v1:'a. (v2:'b. or Thm* ( hbool. ,(v1:'a. (v2:'b. (equal Thm* ( hbool. ,(v1:'a. (v2:'b. ((f Thm* ( hbool. ,(v1:'a. (v2:'b. (,b:hbool. x:'a. y:'b. and(equal(x,v1),b)) Thm* ( hbool. ,(v1:'a. (v2:'b. ,equal Thm* ( hbool. ,(v1:'a. (v2:'b. ,(f Thm* ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. and Thm* ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. (equal(y,v2) Thm* ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. ,not(b))))))))	[his_sum_rep_wd]

In prior sections: hol bool

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