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