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