1signature Norm_ineqs =
2sig
3 type int = Arbint.int
4 type term = Term.term
5 type conv = Abbrev.conv
6
7 val ADD_TERM_TO_LEQ_CONV : term -> conv
8 val ADD_COEFFS_TO_LEQ_CONV : (int * (string * int) list) -> conv
9 val LESS_OR_EQ_GATHER_CONV : conv
10 val ARITH_FORM_NORM_CONV : conv
11end
12