----------------------------------------------------------------------
BIT_ss                                                      (wordsLib)
----------------------------------------------------------------------
BIT_ss : ssfrag

SYNOPSIS
Simplification fragment for words.

KEYWORDS
simplification, words.

DESCRIBE
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
wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.SIZES_ss,
wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss,
wordsLib.WORD_SHIFT_ss, wordsLib.WORD_ARITH_EQ_ss,
wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss,
wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss.

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