----------------------------------------------------------------------
WORD_LOGIC_CONV                                             (wordsLib)
----------------------------------------------------------------------
WORD_LOGIC_CONV : conv

SYNOPSIS
Conversion based on {WORD_LOGIC_ss}.

DESCRIBE
The conversion {WORD_LOGIC_CONV} converts word logic expressions into a
canonical form.

EXAMPLE

- WORD_LOGIC_CONV ``a && (b !! ~a !! c)``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- a && (b !! ~a !! c) = a && b !! a && c : thm


SEEALSO
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.

----------------------------------------------------------------------