(2steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hhd
nuprl
'a
:S,
l
:
'a
List.
mt(
l
)
hd(
l
) = head(
l
)
By:
Unab [`hhd`] THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
'a
: S
2.
l
:
'a
List
3.
mt(
l
)
if null(
l
) then arb(
'a
) else head(
l
) fi = head(
l
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
'a:S, l:'a List. 
mt(l) 
hd(l) = head(l) 'a:S, l:'a List. mt(l) hd(l) = head(l)mt(l)
if null(l) then arb('a) else head(l) fi = head(l)
