1signature ARM_proverLib =
2sig
3
4    val global_mode : Parse.term ref
5    val simp_thms_list : Theory.thm list ref
6    val mode_changing_comp_list : Parse.term list ref
7    val mode_changing_comp_list_rec
8        : Term.term list -> Term.term -> bool
9    val generate_uncurry_abs
10        : Theory.term -> Theory.term list * Theory.term
11    val decompose_term
12        : boolSyntax.term -> boolSyntax.term * boolSyntax.term * boolSyntax.term
13    val get_monad_type  : Type.hol_type -> Type.hol_type
14    val generate_uncurry_abs_from_abs
15        : Theory.term -> Theory.term list * Theory.term
16    val get_type_inst  : Type.hol_type * bool -> Type.hol_type
17    val get_uncurried_theorem  : Thm.thm -> int -> Thm.thm
18    val generalize_theorem  : Abbrev.thm -> Abbrev.term -> Thm.thm
19
20    val prove
21        :
22        Hol_pp.term ->
23        Parse.term ->
24        Parse.term ->
25        Term.term list -> Abbrev.thm list -> Abbrev.thm * Abbrev.tactic
26
27end
28