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