WORD_LOGIC_CONV
wordsLib.WORD_LOGIC_CONV : conv
Conversion based on WORD_LOGIC_ss.
The conversion WORD_LOGIC_CONV converts word logic expressions into a
canonical form.
Example
> wordsLib.WORD_LOGIC_CONV “a && (b !! ~a !! c)”
val it = ⊢ a && (b ‖ ¬a ‖ c) = a && b ‖ a && c: thm
See also
wordsLib.WORD_LOGIC_ss,
wordsLib.WORD_ARITH_CONV,
wordsLib.WORD_MUL_LSL_CONV,
wordsLib.WORD_CONV,
wordsLib.WORD_BIT_EQ_CONV,
wordsLib.WORD_EVAL_CONV