WORD_ARITH_CONV : conv
STRUCTURE
wordsLib
SYNOPSIS
Conversion based on WORD_ARITH_ss and WORD_ARITH_EQ_ss.
DESCRIPTION
The conversion WORD_ARITH_CONV converts word arithmetic expressions into a canonical form.
EXAMPLE
WORD_ARITH_CONV fixes the sign of equalities. 
- SIMP_CONV (std_ss++WORD_ARITH_ss++WORD_ARITH_EQ_ss) [] ``$- a = b : 'a word``
> val it = |- ($- a = b) = ($- 1w * a + $- 1w * b = 0w) : thm

- WORD_ARITH_CONV ``$- a = b : 'a word``
> val it = |- ($- a = b) = (a + b = 0w) : thm
COMMENTS
The fragment WORD_ARITH_EQ_ss and conversion WORD_CONV do not adjust the sign of equalities.
SEEALSO
WORD_ARITH_ss, WORD_ARITH_EQ_ss, WORD_LOGIC_CONV, WORD_MUL_LSL_CONV, WORD_CONV, WORD_BIT_EQ_CONV, WORD_EVAL_CONV
HOL  Trindemossen-1