WORD_LOGIC_CONV : conv
STRUCTURE
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
HOL  Kananaskis-14