----------------------------------------------------------------------
FINITE_CONV                                              (pred_setLib)
----------------------------------------------------------------------
FINITE_CONV : conv

SYNOPSIS
Proves finiteness of sets of the form {{t1;...;tn}}.

LIBRARY
pred_set

DESCRIBE
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}}.

----------------------------------------------------------------------