freesl : term list -> term list
- SYNOPSIS
-
Returns a list of the free variables in a list of terms.
- DESCRIPTION
-
When applied to a list of terms, freesl returns a list of the variables which
are free in any of those terms. There are no repetitions in the list produced
even if several terms contain the same free variable.
- FAILURE CONDITIONS
-
Never fails.
- EXAMPLE
-
In the following example there are free instances of each of w, x and y,
whereas the only instances of z are bound:
# freesl [`x + y = 2`; `!z. z >= x - w`];;
val it : term list = [`y`; `x`; `w`]
- SEE ALSO
-
frees, free_in, thm_frees.