Conversion to produce sign of an integer literal of type :int.
DESCRIPTION
The call INT_SGN_CONV `int_sgn c`, where c is an integer literal of type
:int, returns the theorem |- int_sgn c = d where d is the canonical
integer literal that is equal to c's sign. The literal c may be
of the form &n or -- &n and the result will be of the same form.
FAILURE CONDITIONS
Fails if applied to a term that is not the negation of one of the permitted
forms of integer literal of type :int.
EXAMPLE
# INT_SGN_CONV `int_sgn(-- &42:int)`;;
val it : thm = |- int_sgn (-- &42) = -- &1