WORD_CONV : conv
STRUCTURE
wordsLib
SYNOPSIS
Conversion for words.
DESCRIPTION
The conversion WORD_CONV applies the simpset fragment WORD_ss.
EXAMPLE
- WORD_CONV ``c * (a + b) !! (b + a) * c``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- c * (a + b) !! (b + a) * c = a * c + b * c : thm
SEEALSO
WORD_ss, WORD_ARITH_CONV, WORD_LOGIC_CONV, WORD_MUL_LSL_CONV, WORD_BIT_EQ_CONV, WORD_EVAL_CONV
HOL  Trindemossen-1