Proves finiteness of sets of the form {t1;...;tn}.
LIBRARY
pred_set
DESCRIPTION
The conversion FINITE_CONV expects its term argument to be an assertion of
the form FINITE {t1;...;tn}. Given such a term, the conversion returns
the theorem
|- FINITE {t1;...;tn} = T
EXAMPLE
- FINITE_CONV ``FINITE {1;2;3}``;
> val it = |- FINITE{1;2;3} = T : thm
- FINITE_CONV ``FINITE ({}:num->bool)``;
> val it = |- FINITE {} = T : thm
FAILURE
Fails if applied to a term not of the form FINITE {t1;...;tn}.