all_varsl : term list -> term list
STRUCTURE
Term
SYNOPSIS
Returns the set of all variables in a list of terms.
DESCRIPTION
An invocation all_varsl [t1,...,tn] returns a list representing the set of all term variables occurring in t1,...,tn.
FAILURE
Never fails.
EXAMPLE
- all_varsl [Term `x /\ y /\ y ==> x`,
             Term `!a. a ==> p ==> y`];
> val it = [`x`, `y`, `p`, `a`] : term list

COMMENTS
Code should not depend on how elements are arranged in the result of all_varsl.
SEEALSO
all_atoms, all_vars, empty_varset, free_vars_lr, free_vars, free_varsl, FVL, type_vars
HOL  Trindemossen-1