# Structure transcSyntax

signature transcSyntax =
sig
type term = Term.term
val Dint_tm: term
val acs_tm: term
val asn_tm: term
val atn_tm: term
val cos_tm: term
val division_tm: term
val dsize_tm: term
val exp_tm: term
val fine_tm: term
val gauge_tm: term
val ln_tm: term
val pi_tm: term
val root_tm: term
val rpow_tm: term
val rsum_tm: term
val sin_tm: term
val sqrt_tm: term
val tan_tm: term
val tdiv_tm: term
val dest_Dint: term -> term * term * term
val dest_acs: term -> term
val dest_asn: term -> term
val dest_atn: term -> term
val dest_cos: term -> term
val dest_division: term -> term * term
val dest_dsize: term -> term
val dest_exp: term -> term
val dest_fine: term -> term * term
val dest_gauge: term -> term * term
val dest_ln: term -> term
val dest_root: term -> term * term
val dest_rpow: term -> term * term
val dest_rsum: term -> term * term
val dest_sin: term -> term
val dest_sqrt: term -> term
val dest_tan: term -> term
val dest_tdiv: term -> term * term
val is_Dint: term -> bool
val is_acs: term -> bool
val is_asn: term -> bool
val is_atn: term -> bool
val is_cos: term -> bool
val is_division: term -> bool
val is_dsize: term -> bool
val is_exp: term -> bool
val is_fine: term -> bool
val is_gauge: term -> bool
val is_ln: term -> bool
val is_root: term -> bool
val is_rpow: term -> bool
val is_rsum: term -> bool
val is_sin: term -> bool
val is_sqrt: term -> bool
val is_tan: term -> bool
val is_tdiv: term -> bool
val mk_Dint: term * term * term -> term
val mk_acs: term -> term
val mk_asn: term -> term
val mk_atn: term -> term
val mk_cos: term -> term
val mk_division: term * term -> term
val mk_dsize: term -> term
val mk_exp: term -> term
val mk_fine: term * term -> term
val mk_gauge: term * term -> term
val mk_ln: term -> term
val mk_root: term * term -> term
val mk_rpow: term * term -> term
val mk_rsum: term * term -> term
val mk_sin: term -> term
val mk_sqrt: term -> term
val mk_tan: term -> term
val mk_tdiv: term * term -> term
end

*HOL 4, Kananaskis-13*