PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hisl
wd
'b
,
'a
:S. and(all(
x
:
'a
. isl(inl(
x
))),all(
y
:
'b
. not(isl(inr(
y
)))))
By:
Unab [`hisl`] THEN HN THEN Try (Complete Auto)
THEN
Try (Complete (Unfold `label` 0))
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
'b,'a:S. and(all(
x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y))))) 'b,'a:S. and(all(x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y)))))
