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