butlast : 'a list -> 'a list
STRUCTURE
SYNOPSIS
Computes the sub-list of a list consisting of all but the last element.
DESCRIPTION
butlast [x1,...,xn] returns [x1,...,x(n-1)].
FAILURE
Fails if the list is empty.
SEEALSO
HOL  Kananaskis-10