REVERSE_CONV : conv
STRUCTURE
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
HOL  Kananaskis-10