1signature jbUtils = 2sig 3 type term = Term.term 4 type thm = Thm.thm 5 type goal = Abbrev.goal 6 type conv = Abbrev.conv 7 type tactic = Abbrev.tactic 8 type hol_type = Abbrev.hol_type 9 10 val AND_IMP_RULE: thm -> thm 11 val IMP_AND_RULE: thm -> thm 12 13 val REWRITE1_TAC: thm -> tactic 14 val ONCE_REWRITE1_TAC: thm -> tactic 15 val PROVE1_TAC: thm -> tactic 16 val ASSUME_X_TAC: thm -> tactic 17 val DISJ_LIST_CASES_TAC: thm -> tactic 18 val NESTED_ASM_CASES_TAC: term list -> tactic 19 20 val REMAINS_TO_PROVE: term -> tactic 21 val NEW_GOAL_TAC: term -> tactic 22 23 val extract_terms_of_type : hol_type -> term -> term list 24 val store_thm_verbose : string * term * tactic -> thm 25 val dest_binop_triple : term -> term * term * term 26end 27