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