line_var : (term -> term)
STRUCTURE
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
HOL  Trindemossen-1