1\DOC 2 3\TYPE {BIT_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {BIT_ss} rewrites the term {``BIT i n``} for ground {n}. 16 17\EXAMPLE 18{ 19- SIMP_CONV (std_ss++BIT_ss) [] ``BIT i 33``; 20> val it = |- BIT i 33 = i IN {0; 5} : thm 21 22- SIMP_CONV (std_ss++BIT_ss) [] ``BIT 5 33``; 23> val it = |- BIT 5 33 = T : thm 24} 25 26\SEEALSO 27 28wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, 29wordsLib.WORD_LOGIC_ss, wordsLib.WORD_SHIFT_ss, wordsLib.WORD_ARITH_EQ_ss, 30wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss, wordsLib.WORD_MUL_LSL_ss, 31wordsLib.WORD_ss 32 33\ENDDOC 34