1signature Solve_ineqs =
2sig
3  type int = Arbint.int
4  type term = Term.term
5  type thm  = Thm.thm
6  type conv = Abbrev.conv
7
8  val CONST_TIMES_ARITH_CONV : conv
9  val MULT_LEQ_BY_CONST_CONV : term -> conv
10  val LEQ_CONV : conv
11  val WEIGHTED_SUM :
12         string ->
13         ((int * (string * int) list) * (int * (string * int) list)) ->
14         ((int * (string * int) list) * (unit -> thm))
15  val var_to_elim : ('a * (string * int) list) list -> string
16  val VAR_ELIM :
17         (int * (string * int) list) list -> (int list * (unit -> thm))
18end
19