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