1signature reduceLib =
2sig
3    include Abbrev
4
5    val NOT_CONV    : conv
6    val AND_CONV    : conv
7    val OR_CONV     : conv
8    val IMP_CONV    : conv
9    val BEQ_CONV    : conv
10    val COND_CONV   : conv
11
12    val NEQ_CONV    : conv
13    val LT_CONV     : conv
14    val GT_CONV     : conv
15    val LE_CONV     : conv
16    val GE_CONV     : conv
17    val ODD_CONV    : conv
18    val EVEN_CONV   : conv
19    val SUC_CONV    : conv
20    val PRE_CONV    : conv
21    val SBC_CONV    : conv
22    val ADD_CONV    : conv
23    val MUL_CONV    : conv
24    val EXP_CONV    : conv
25    val DIV_CONV    : conv
26    val MOD_CONV    : conv
27
28    val RED_CONV    : conv
29    val REDUCE_CONV : conv
30    val REDUCE_RULE : thm -> thm
31    val REDUCE_TAC  : tactic
32
33    val num_compset : unit -> computeLib.compset
34end
35