1signature fracLib =
2sig
3        type term = Term.term
4        type thm = Thm.thm
5        type goal = Abbrev.goal
6        type conv = Abbrev.conv
7        type tactic = Abbrev.tactic
8        type simpset = simpLib.simpset
9
10        (* equivalence *)
11        val FRAC_EQ_CONV : conv
12        val FRAC_NOTEQ_CONV : conv
13        val FRAC_EQ_TAC : tactic
14
15        (* positive and non-zero *)
16        val FRAC_POS_CONV : conv
17        val FRAC_NOT0_CONV : conv
18        val FRAC_POS_TAC : term -> tactic
19        val FRAC_NOT0_TAC : term -> tactic
20
21        (* numerator and denominator extraction *)
22        val FRAC_NMR_CONV : conv
23        val FRAC_DNM_CONV : conv
24        val FRAC_NMRDNM_TAC : tactic
25
26        (* calculation *)
27        val FRAC_CALC_CONV : conv
28        val FRAC_STRICT_CALC_TAC : tactic
29        val FRAC_CALCTERM_TAC : term -> tactic
30        val FRAC_CALC_TAC : tactic
31
32        val FRAC_STRICT_CALCEQ_TAC : tactic
33        val FRAC_CALCEQ_TAC : tactic
34
35        val FRAC_SAVE_CONV : conv
36        val FRAC_SAVE_TAC : tactic
37
38end
39