WORD_CONV

wordsLib.WORD_CONV : conv

Conversion for words.

The conversion WORD_CONV applies the simpset fragment WORD_ss.

Example

> wordsLib.WORD_CONV “c * (a + b) !! (b + a) * c”
val it = ⊢ c * (a + b) ‖ (b + a) * c = a * c + b * c: thm

See also

wordsLib.WORD_ss, wordsLib.WORD_ARITH_CONV, wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_EVAL_CONV