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