1signature Psyntax = 2sig 3 type hol_type = Type.hol_type 4 type term = Term.term 5 6 7 val mk_type : string * hol_type list -> hol_type 8 val mk_var : string * hol_type -> term 9 val mk_primed_var : string * hol_type -> term 10 val mk_const : string * hol_type -> term 11 val mk_abs : term * term -> term 12 val mk_comb : term * term -> term 13 val mk_cond : term * term * term -> term 14 val mk_conj : term * term -> term 15 val mk_disj : term * term -> term 16 val mk_eq : term * term -> term 17 val mk_forall : term * term -> term 18 val mk_exists : term * term -> term 19 val mk_exists1 : term * term -> term 20 val mk_select : term * term -> term 21 val mk_imp : term * term -> term 22 val mk_let : term * term -> term 23 24 val dest_type : hol_type -> string * hol_type list 25 val dest_var : term -> string * hol_type 26 val dest_const : term -> string * hol_type 27 val dest_abs : term -> term * term 28 val dest_comb : term -> term * term 29 val dest_cond : term -> term * term * term 30 val dest_conj : term -> term * term 31 val dest_disj : term -> term * term 32 val dest_eq : term -> term * term 33 val dest_forall : term -> term * term 34 val dest_exists : term -> term * term 35 val dest_exists1 : term -> term * term 36 val dest_select : term -> term * term 37 val dest_imp : term -> term * term 38 val dest_imp_only : term -> term * term 39 val dest_let : term -> term * term 40 41 val new_type : string * int -> unit 42 val new_constant : string * hol_type -> unit 43 val new_infix : string * hol_type * int -> unit 44 val new_binder : string * hol_type -> unit 45 46 datatype lambda = datatype Term.lambda 47 48 val dest_term : term -> lambda 49end 50