(4steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mt
append
1
1.
'a
: Type
2.
l
:
'a
List
3.
ll
:
'a
List
4. mt(
l
@
ll
)
mt(
l
)
By:
Last MoveToConcl THEN Analyze 3 THEN Analyze 2 THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc