PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hisl
or
isr
'a
,
'b
:S. all(
x
:hsum(
'a
;
'b
). or(isl(
x
),isr(
x
)))
By:
HOL "hisl_or_isr"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
'a,'b:S. all(
x:hsum('a; 'b). or(isl(x),isr(x)))
