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