PrintForm Definitions Lemmas hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: isl or isr
  'a,'b:S, x:'a+'b. isl(x)  isr(x)
By: RewriteOfThm Thm* 'a,'b:S. all(x:hsum('a; 'b). or(isl(x),isr(x))) HNC

Generated subgoals:

None

About:
assertunionapplyorall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas hol sum Sections HOLlib Doc