FINITE_CONV : conv
STRUCTURE
SYNOPSIS
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}.
HOL  Kananaskis-13