1signature fracSyntax = 2sig 3 type term = Term.term 4 type hol_type = Abbrev.hol_type 5 6 val frac : hol_type 7 8 val frac_0_tm : term 9 val frac_1_tm : term 10 11 val frac_nmr_tm : term 12 val frac_dnm_tm : term 13 val frac_sgn_tm : term 14 val frac_ainv_tm : term 15 val frac_minv_tm : term 16 val frac_add_tm : term 17 val frac_sub_tm : term 18 val frac_mul_tm : term 19 val frac_div_tm : term 20 21 val mk_frac_nmr : term -> term 22 val mk_frac_dnm : term -> term 23 val mk_frac_sgn : term -> term 24 val mk_frac_ainv : term -> term 25 val mk_frac_minv : term -> term 26 val mk_frac_add : term * term -> term 27 val mk_frac_sub : term * term -> term 28 val mk_frac_mul : term * term -> term 29 val mk_frac_div : term * term -> term 30 31 val dest_frac_nmr : term -> term 32 val dest_frac_dnm : term -> term 33 val dest_frac_sgn : term -> term 34 val dest_frac_ainv : term -> term 35 val dest_frac_minv : term -> term 36 val dest_frac_add : term -> term * term 37 val dest_frac_sub : term -> term * term 38 val dest_frac_mul : term -> term * term 39 val dest_frac_div : term -> term * term 40 41 val is_frac_nmr : term -> bool 42 val is_frac_dnm : term -> bool 43 val is_frac_sgn : term -> bool 44 val is_frac_ainv : term -> bool 45 val is_frac_minv : term -> bool 46 val is_frac_add : term -> bool 47 val is_frac_sub : term -> bool 48 val is_frac_mul : term -> bool 49 val is_frac_div : term -> bool 50 51end 52