WORD_LOGIC_CONV : conv
STRUCTURE
wordsLib
SYNOPSIS
Conversion based on WORD_LOGIC_ss.
DESCRIPTION
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
WORD_LOGIC_ss, WORD_ARITH_CONV, WORD_MUL_LSL_CONV, WORD_CONV, WORD_BIT_EQ_CONV, WORD_EVAL_CONV
HOL  Kananaskis-14