line_var : (term -> term)
STRUCTURE
unwindLib
SYNOPSIS
Computes the line variable of an equation.
LIBRARY
unwind
DESCRIPTION
line_var "!y1 ... ym. f x1 ... xn = t"
returns the variable
"f"
.
FAILURE
Fails if the argument term is not of the specified form.
SEEALSO
line_name
HOL
Kananaskis-14