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