WORD_BIT_EQ_CONV : conv
STRUCTURE
SYNOPSIS
Conversion based on WORD_BIT_EQ_ss.
DESCRIPTION
The conversion WORD_BIT_EQ_CONV performs simplification using fcpLib.FCP_ss.
EXAMPLE
- WORD_BIT_EQ_CONV ``a << 2 >>> 1 = ((5 -- 0) a << 1) :word8``
> val it = |- (a << 2 >>> 1 = (5 -- 0) a << 1) = T : thm
SEEALSO
HOL  Kananaskis-13