BIT_ss : ssfrag
STRUCTURE
wordsLib
SYNOPSIS
Simplification fragment for words.
DESCRIPTION
The fragment BIT_ss rewrites the term ``BIT i n`` for ground n.
EXAMPLE
- SIMP_CONV (std_ss++BIT_ss) [] ``BIT i 33``;
> val it = |- BIT i 33 = i IN {0; 5} : thm

- SIMP_CONV (std_ss++BIT_ss) [] ``BIT 5 33``;
> val it = |- BIT 5 33 = T : thm
SEEALSO
WORD_CONV, FCP_ss, SIZES_ss, WORD_ARITH_ss, WORD_LOGIC_ss, WORD_SHIFT_ss, WORD_ARITH_EQ_ss, WORD_BIT_EQ_ss, WORD_EXTRACT_ss, WORD_MUL_LSL_ss, WORD_ss
HOL  Kananaskis-13