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