1signature wordsLib =
2sig
3    include Abbrev
4
5    val words_compset       : unit -> computeLib.compset
6
7    val SIZES_ss            : simpLib.ssfrag
8    val BIT_ss              : simpLib.ssfrag
9    val BITS_INTRO_ss       : simpLib.ssfrag
10    val WORD_ARITH_ss       : simpLib.ssfrag
11    val WORD_LOGIC_ss       : simpLib.ssfrag
12    val WORD_SUB_ss         : simpLib.ssfrag
13    val WORD_SHIFT_ss       : simpLib.ssfrag
14    val WORD_ARITH_EQ_ss    : simpLib.ssfrag
15    val WORD_CANCEL_ss      : simpLib.ssfrag
16    val WORD_BIT_EQ_ss      : simpLib.ssfrag
17    val WORD_EXTRACT_ss     : simpLib.ssfrag
18    val WORD_MUL_LSL_ss     : simpLib.ssfrag
19    val WORD_UINT_MAX_ss    : simpLib.ssfrag
20    val WORD_CONCAT_ASSOC_ss: simpLib.ssfrag
21    val WORD_GROUND_ss      : simpLib.ssfrag
22    val WORD_ss             : simpLib.ssfrag
23
24    val LESS_CONV           : conv
25    val SIZES_CONV          : conv
26    val word_EQ_CONV        : conv
27    val UINT_MAX_CONV       : conv
28    val BIT_SET_CONV        : conv
29    val BITS_INTRO_CONV     : conv
30    val WORD_ARITH_CONV     : conv
31    val WORD_ADD_CANON_CONV : conv
32    val WORD_CANCEL_CONV    : conv
33    val WORD_LOGIC_CONV     : conv
34    val WORD_SUB_CONV       : conv
35    val WORD_MUL_LSL_CONV   : conv
36    val WORD_DIV_LSR_CONV   : conv
37    val WORD_MOD_BITS_CONV  : conv
38    val WORD_CONV           : conv
39    val WORD_BIT_EQ_CONV    : conv
40    val WORD_BIT_INDEX_CONV : bool -> conv
41    val EXTEND_EXTRACT_CONV : conv
42    val EXPAND_REDUCE_CONV  : conv
43
44    val n2w_INTRO_TAC       : int -> tactic
45
46    val WORD_DP             : conv -> conv -> conv
47    val WORD_ARITH_PROVE    : conv
48    val WORD_DECIDE         : conv
49    val WORD_DECIDE_TAC     : tactic
50
51    val add_words_compset   : bool -> computeLib.compset -> unit
52
53    val WORD_GROUND_CONV    : conv
54    val WORD_EVAL_CONV      : conv
55    val WORD_EVAL_RULE      : rule
56    val WORD_EVAL_TAC       : tactic
57
58    val Induct_word         : tactic
59    val Cases_word          : tactic
60    val Cases_word_value    : tactic
61    val Cases_on_word       : term frag list -> tactic
62    val Cases_on_word_value : term frag list -> tactic
63
64    val mk_word_size        : int -> unit
65    val dest_word_literal   : term -> Arbnum.num
66
67    val prefer_word         : unit -> unit
68    val deprecate_word      : unit -> unit
69
70    val output_words_as_bin : unit -> unit
71    val output_words_as_oct : unit -> unit
72    val output_words_as_hex : unit -> unit
73    val output_words_as_dec : unit -> unit
74
75    val output_words_as_padded_bin : unit -> unit
76    val output_words_as_padded_hex : unit -> unit
77
78    val remove_word_printer : unit -> unit
79
80    val add_word_cast_printer       : unit -> unit
81    val remove_word_cast_printer    : unit -> unit
82
83    val guessing_word_lengths       : bool ref
84    val notify_on_word_length_guess : bool ref
85    val inst_word_lengths           : term -> term
86    val guess_lengths               : unit -> unit
87end
88