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