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