1signature Rsyntax = 2sig 3 type hol_type = Type.hol_type 4 type term = Term.term 5 type thm = Thm.thm 6 7 val mk_type : {Args:hol_type list, Tyop:string} -> hol_type 8 val mk_var : {Name:string, Ty:hol_type} -> term 9 val mk_primed_var : {Name:string, Ty:hol_type} -> term 10 val mk_const : {Name:string, Ty:hol_type} -> term 11 val mk_abs : {Bvar:term, Body:term} -> term 12 val mk_comb : {Rand:term, Rator:term} -> term 13 val mk_cond : {cond:term, larm:term, rarm:term} -> term 14 val mk_conj : {conj1:term, conj2:term} -> term 15 val mk_disj : {disj1:term, disj2:term} -> term 16 val mk_eq : {lhs:term, rhs:term} -> term 17 val mk_forall : {Bvar:term, Body:term} -> term 18 val mk_exists : {Bvar:term, Body:term} -> term 19 val mk_exists1 : {Bvar:term, Body:term} -> term 20 val mk_select : {Bvar:term, Body:term} -> term 21 val mk_imp : {ant:term, conseq:term} -> term 22 val mk_let : {arg:term, func:term} -> term 23 24 val dest_type : hol_type -> {Args:hol_type list, Tyop:string} 25 val dest_var : term -> {Name:string, Ty:hol_type} 26 val dest_const : term -> {Name:string, Ty:hol_type} 27 val dest_abs : term -> {Body:term, Bvar:term} 28 val dest_comb : term -> {Rand:term, Rator:term} 29 val dest_cond : term -> {cond:term, larm:term, rarm:term} 30 val dest_conj : term -> {conj1:term, conj2:term} 31 val dest_disj : term -> {disj1:term, disj2:term} 32 val dest_eq : term -> {lhs:term, rhs:term} 33 val dest_forall : term -> {Bvar:term, Body:term} 34 val dest_exists : term -> {Bvar:term, Body:term} 35 val dest_exists1 : term -> {Bvar:term, Body:term} 36 val dest_select : term -> {Bvar:term, Body:term} 37 val dest_imp : term -> {ant:term, conseq:term} 38 val dest_imp_only : term -> {ant:term, conseq:term} 39 val dest_let : term -> {arg:term, func:term} 40 41 val new_type : {Arity:int, Name:string} -> unit 42 val new_constant : {Name:string, Ty:hol_type} -> unit 43 val new_infix : {Name:string, Prec:int, Ty:hol_type} -> unit 44 val new_binder : {Name:string, Ty:hol_type} -> unit 45 val new_specification : {name : string, 46 sat_thm : thm, 47 consts : {const_name : string, 48 fixity : Parse.fixity option} list} -> thm 49 datatype lambda 50 = VAR of {Name:string, Ty:hol_type} 51 | CONST of {Name:string, Thy:string, Ty:hol_type} 52 | COMB of {Rator:term, Rand:term} 53 | LAMB of {Bvar:term, Body:term}; 54 55 val dest_term : term -> lambda 56end 57