1signature utilsLib = 2sig 3 include Abbrev 4 5 type inventory = {C: string list, N: int list, T: string list, Thy: string} 6 type cover = {redex: term frag list, residue: term} list list 7 8 val ALL_HYP_CONV_RULE: conv -> rule 9 val ALL_HYP_RULE: rule -> rule 10 val BIT_FIELD_INSERT_CONV : string -> string -> conv 11 val CASE_RAND_CONV : term -> conv 12 val CHANGE_CBV_CONV: computeLib.compset -> conv 13 val ELIM_UNDISCH: rule 14 val EXTRACT_CONV: conv 15 val FULL_CONV_RULE: conv -> thm -> thm 16 val HYP_CANON_RULE: rule 17 val HYP_CONV_RULE: conv -> term -> rule 18 val HYP_RULE: (thm -> thm) -> term -> rule 19 val INST_REWRITE_CONV: thm list -> conv 20 val INST_REWRITE_CONV1: thm -> conv 21 val INST_REWRITE_RULE: thm list -> rule 22 val LIST_DISCH: term list -> rule 23 val MATCH_HYP_CONV_RULE: conv -> term -> rule 24 val MATCH_HYP_RULE: rule -> term -> rule 25 val MERGE_CASES: term -> thm -> thm -> thm 26 val NCONV: int -> conv -> conv 27 val PRED_HYP_CONV_RULE: conv -> (term -> bool) -> rule 28 val PRED_HYP_RULE: rule -> (term -> bool) -> rule 29 val REC_REG_BIT_FIELD_INSERT_TAC: 30 string -> string -> term quotation -> tactic 31 val Run_CONV: string * term -> conv 32 val SET_CONV: conv 33 val SET_RULE: rule 34 val SRW_CONV: thm list -> conv 35 val SRW_RULE: thm list -> rule 36 val STEP: 37 (thm list -> thm list) * term -> thm list -> term list list -> cover -> 38 term -> thm list 39 val STRIP_UNDISCH: rule 40 val WGROUND_CONV: conv 41 val accessor_fns: hol_type -> term list 42 val accessor_update_fns: hol_type -> (term * term) list 43 val add_base_datatypes: computeLib.compset -> unit 44 val add_datatypes: hol_type list -> computeLib.compset -> unit 45 val add_theory: (thm list * inventory) -> computeLib.compset -> unit 46 val add_to_rw_net: 47 (thm -> term) -> thm * thm LVTermNet.lvtermnet -> thm LVTermNet.lvtermnet 48 val add_to_the_compset: (thm list * inventory) -> unit 49 val adjoin_thms: unit -> unit 50 val augment: term frag list * term list -> cover -> cover 51 val avoid_name_clashes: term -> term -> term 52 val cache: int -> ('a * 'a -> order) -> ('a -> 'b) -> 'a -> 'b 53 val classes: ('a * 'a -> bool) -> 'a list -> 'a list list 54 val datatype_rewrites: bool -> string -> string list -> thm list 55 val dom: hol_type -> hol_type 56 val eval: term -> term 57 val filter_inventory: string list -> inventory -> inventory 58 val find_rw: thm LVTermNet.lvtermnet -> term -> thm list 59 val for_thm: int * int -> thm 60 val get_function: thm -> term 61 val lhsc: thm -> term 62 val list_mk_wordii: int -> int list -> term list 63 val long_term_to_string: term -> string 64 val lowercase: string -> string 65 val map_conv: conv -> term list -> thm 66 val match_subst: {redex: term, residue: term} list -> term -> term 67 val maximal: ('a * 'a -> order) -> ('b -> 'a) -> 'b list -> 'b * 'b list 68 val minimal: ('a * 'a -> order) -> ('b -> 'a) -> 'b list -> 'b * 'b list 69 val mk_cond_exhaustive_thm: int -> thm 70 val mk_cond_rand_thms: term list -> thm 71 val mk_cond_update_thms: hol_type list -> thm list 72 val mk_negation: term -> term 73 val mk_reg_thm: string -> string -> thm 74 val mk_run: string * term -> term -> term 75 val mk_rw_net: (thm -> term) -> thm list -> thm LVTermNet.lvtermnet 76 val mk_state_id_thm: thm -> string list list -> thm 77 val o_RULE: rule 78 val padLeft: 'a -> int -> 'a list -> 'a list 79 val partitions: 'a list -> 'a list list list 80 val pattern: string -> term 81 val pick: bool list -> 'a list -> 'a list 82 val print_options: int option -> string -> string list list -> unit 83 val process_opt: 84 ''a list list -> string -> 'b -> ''a list -> (int -> 'b) -> 'b * ''a list 85 val process_option: 86 ('a -> bool) -> ('a -> ''b) -> string -> 'c -> 'a list -> (''b -> 'c) -> 87 'c * 'a list 88 val qm: thm list -> term -> thm 89 val qm_tac: thm list -> tactic 90 val removeSpaces: string -> string 91 val resetStepConv: unit -> unit 92 val reset_thms: unit -> unit 93 val rev_endian: 'a list -> 'a list 94 val rhsc: thm -> term 95 val rng: hol_type -> hol_type 96 val save_as: string -> thm -> thm 97 val save_thms: string -> thm list -> thm list 98 val setStepConv: conv -> unit 99 val specialized: string -> conv * term list -> thm list -> thm list 100 val splitAtChar: (char -> bool) -> string -> string * string 101 val splitAtPos: int -> string -> string * string 102 val split_conditions: thm -> thm list 103 val strip_add_or_sub: term -> term * (bool * term) list 104 val strings_to_quote: string list -> string frag list 105 val tab_fixedwidth: int -> int -> term list 106 val theory_compset: (thm list * inventory) -> computeLib.compset 107 val theory_rewrites: (thm list * inventory) -> thm list 108 val theory_types: inventory -> hol_type list 109 val update_fns: hol_type -> term list 110 val uppercase: string -> string 111 val usave_as: string -> thm -> thm 112 val ustore_thm: string * Q.tmquote * tactic -> thm 113 val vacuous: thm -> bool 114 val zipLists: ('a list -> 'b) -> 'a list list -> 'b list 115end 116