1signature Term =
2sig
3
4  include FinalTerm where type hol_type = Type.hol_type
5                      and type term = KernelTypes.term
6  val prim_mk_eq        : hol_type -> term -> term -> term
7  val prim_mk_imp       : term -> term -> term
8  val imp               : term
9  val dest_eq_ty        : term -> term * term * hol_type
10  val lazy_beta_conv    : term -> term
11  val kernelid          : string
12
13end
14