1signature Term =
2sig
3
4  include FinalTerm where type hol_type = KernelTypes.hol_type
5                          and type term = KernelTypes.term
6
7  val termsig        : KernelTypes.holty KernelSig.symboltable
8
9  val lazy_beta_conv : term -> term
10  val imp            : term
11  val dest_eq_ty     : term -> term * term * hol_type
12  val prim_mk_eq     : hol_type -> term -> term -> term
13  val prim_mk_imp    : term -> term -> term
14  val break_const    : term -> KernelTypes.id * hol_type
15  val break_abs      : term -> term
16  val trav           : (term -> unit) -> term -> unit
17  val is_bvar        : term -> bool
18  val kernelid       : string
19
20end
21