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