1signature ratLib =
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 ssfrag = simpLib.ssfrag
9        type simpset = simpLib.simpset
10
11        (* conversions *)
12        val RAT_EQ_CONV : conv
13        val RAT_CALC_CONV : conv
14        val RAT_ADDAC_CONV :conv
15        val RAT_MULAC_CONV :conv
16
17        (* tactics *)
18        val RAT_EQ_TAC : tactic
19        val RAT_ADDAC_TAC : term -> tactic
20        val RAT_MULAC_TAC : term -> tactic
21        val RAT_EQ_LMUL_TAC : term -> tactic
22        val RAT_EQ_RMUL_TAC : term -> tactic
23        val RAT_ADDSUB_TAC : term -> term -> tactic
24        val RAT_CALCTERM_TAC : term -> tactic
25        val RAT_STRICT_CALC_TAC : tactic
26        val RAT_CALC_TAC : tactic
27        val RAT_CALCEQ_TAC : tactic
28
29        (* conversions *)
30        val RAT_PRECALC_CONV : conv
31        val RAT_POSTCALC_CONV : conv
32        val RAT_BASIC_ARITH_CONV : conv
33        val RAT_ELIMINATE_MINV_EQ_CONV : conv
34        val RAT_ELIMINATE_MINV_CONV : conv
35
36        (* tactics *)
37        val RAT_SAVE_TAC : term -> tactic
38        val RAT_SAVE_ALLVARS_TAC : tactic
39        val RAT_BASIC_ARITH_TAC : tactic
40        val RAT_ELIMINATE_MINV_TAC : tactic
41
42        val int_rewrites : thm list
43        val rat_basic_rewrites : thm list
44        val rat_rewrites : thm list
45        val rat_num_rewrites : thm list
46
47end
48