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