1\DOC FVL 2 3\TYPE {FVL : term list -> term set -> term set} 4 5\SYNOPSIS 6Efficient computation of the set of free variables in a list of terms. 7 8\KEYWORDS 9variable, free, set. 10 11\DESCRIBE 12An invocation {FVL [t1,...,tn] V} adds the set of free variables found 13in {t1,...,tn} to the accumulator {V}. 14 15\FAILURE 16Never fails. 17 18\EXAMPLE 19{ 20- FVL [Term `v1 /\ v2 ==> v2 \/ v3`] empty_varset; 21> val it = <set> : term set 22 23- HOLset.listItems it; 24> val it = [`v1`, `v2`, `v3`] : term list 25} 26 27 28\COMMENTS 29Preferable to {free_varsl} when the number of free variables 30becomes large. 31 32\SEEALSO 33HOLset, Term.empty_varset, Term.free_varsl, Term.free_vars. 34\ENDDOC 35