1signature ARM_prover_extLib =
2sig
3    (* include arm_encoderLib arm_disassemblerLib*)
4
5    val decompose_term
6        : boolSyntax.term -> boolSyntax.term * boolSyntax.term * boolSyntax.term
7    val mk_spec_list  : Parse.term -> Parse.term list
8    val mk_spec_list2  : Parse.term -> Parse.term list
9    val mk_spec_list3  : Parse.term -> Parse.term list
10    val mk_spec_list4  : Parse.term -> Parse.term list
11    val generate_uncurry_abs
12        : Theory.term -> Theory.term list * Theory.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_action_from_goal  : 'a * boolSyntax.term -> boolSyntax.term
17    val find_theorem  : string -> Thm.thm
18    val get_uncurried_theorem  : Thm.thm -> int -> Thm.thm
19    val generalize_theorem  : Abbrev.thm -> Abbrev.term -> Thm.thm
20    val get_type_inst  : Type.hol_type * bool -> Type.hol_type
21    val prove_const :
22        Term.term ->
23        (Abbrev.term -> Term.term list -> 'a) list ->
24        Term.term list ->
25        'b -> string -> Abbrev.thm list -> Abbrev.thm * Abbrev.tactic
26    val get_second_lemmma
27        : Abbrev.thm -> Parse.term -> Parse.term -> Abbrev.thm -> Abbrev.thm
28    val prove_abs_action
29        :
30        Abbrev.term * (Abbrev.term -> Abbrev.term list -> 'a) list *
31        Abbrev.term list * 'b * Thm.thm list *
32        (
33         Abbrev.term ->
34         Abbrev.term list ->
35         Term.term -> Abbrev.thm -> Thm.thm list -> 'c) *
36        ('b -> Abbrev.term list -> Term.term -> 'c -> Abbrev.thm) ->
37        Abbrev.thm * Abbrev.tactic
38
39end
40
41
42
43
44
45
46