REVERSE_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of reversing a list.
DESCRIPTION
REVERSE_CONV takes a term tm in the following form: 
   REVERSE [x0;...xn]
It returns the theorem 
   |- REVERSE [x0;...xn] = [xn;...x0]
where the right-hand side is the list in the reverse order.
FAILURE
REVERSE_CONV tm fails if tm is not of the form described above.
EXAMPLE
Evaluating 
   REVERSE_CONV (--`REVERSE [0;1;2;3;4]`--);
returns the following theorem: 
   |- REVERSE [0;1;2;3;4] = [4;3;2;1;0]
SEEALSO
FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV
HOL  Kananaskis-10