(2steps total)
PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
houtl
nuprl
'a
,
'b
:S,
u
:
'a
+
'b
. isl(
u
)
outl(
u
) = outl(
u
)
By:
Id THEN StrongAuto
Generated subgoal:
1
1.
'a
: S
2.
'b
: S
3.
u
:
'a
+
'b
4. isl(
u
)
outl(
u
) = outl(
u
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
hol
sum
Sections
HOLlib
Doc
'a,'b:S, u:'a+'b. isl(u) 
outl(u) = outl(u) 'a,'b:S, u:'a+'b. isl(u) outl(u) = outl(u) outl(u) = outl(u)
