1signature bitstringLib =
2sig
3    include Abbrev
4
5    val add_bitstring_compset : computeLib.compset -> unit
6
7    val BITSTRING_GROUND_CONV : Conv.conv
8    val BITSTRING_GROUND_ss : simpLib.ssfrag
9    val v2w_n2w_ss : simpLib.ssfrag
10
11    val Cases_on_v2w : term frag list -> tactic
12
13    type bitify_boolify =
14        { bitify_def : thm,
15          bitify_tm : term,
16          mk_bitify : term -> term,
17          dest_bitify : term -> term,
18          is_bitify : term -> bool,
19          boolify_def : thm,
20          boolify_tm : term,
21          mk_boolify : term -> term,
22          dest_boolify : term -> term,
23          is_boolify : term -> bool }
24
25    val FIX_CONV : conv
26    val FIX_v2w_CONV : conv
27    val v2n_CONV : conv
28    val v2w_n2w_CONV : conv
29    val n2w_v2w_CONV : conv
30    val v2w_eq_CONV : conv
31    val word_eq_CONV : conv
32    val extract_v2w_CONV : conv
33    val word_bit_CONV : conv
34
35    val bitify_num : int -> Arbnum.num -> term list
36
37    val bitify_boolify : int -> bitify_boolify
38end
39