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