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