1signature translateLib =
2sig
3        include Abbrev
4
5        val CHOOSEP_TAC             : thm list -> tactic
6        val CHOOSEP                 : thm list -> term -> thm
7        val DOUBLE_MATCH            : (term -> term) -> (term -> term) -> term -> thm -> thm
8
9        val ite_tm                  : term
10        val mk_acl2_cond            : term * term * term -> term
11        val dest_acl2_cond          : term -> term * term * term
12        val is_acl2_cond            : term -> bool
13
14        val acl2_cons_tm            : term
15        val mk_acl2_cons            : term * term -> term
16        val dest_acl2_cons          : term -> term * term
17        val strip_cons              : term -> term list
18
19        val acl2_true_tm            : term
20        val mk_acl2_true            : term -> term
21        val dest_acl2_true          : term -> term
22        val is_acl2_true            : term -> bool
23
24        val DISJ_CASES_UNIONL       : thm -> thm list -> thm
25
26        val RAT_CONG_TAC            : tactic
27
28        val EQUAL_EXISTS_TAC        : tactic
29        val FIX_CI_TAC              : tactic
30
31end
32