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