1\DOC 2 3\TYPE {WORD_CONV : conv} 4 5\SYNOPSIS 6 7Conversion for words. 8 9\DESCRIBE 10 11The conversion {WORD_CONV} applies the simpset fragment {WORD_ss}. 12 13\EXAMPLE 14{ 15- WORD_CONV ``c * (a + b) !! (b + a) * c`` 16<<HOL message: inventing new type variable names: 'a>> 17> val it = |- c * (a + b) !! (b + a) * c = a * c + b * c : thm 18} 19 20\SEEALSO 21 22wordsLib.WORD_ss, wordsLib.WORD_ARITH_CONV, wordsLib.WORD_LOGIC_CONV, 23wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_EVAL_CONV 24 25\ENDDOC 26