# let REAL_POLY_NEG_CONV,REAL_POLY_ADD_CONV,REAL_POLY_SUB_CONV,
REAL_POLY_MUL_CONV,REAL_POLY_POW_CONV,REAL_POLY_CONV =
SEMIRING_NORMALIZERS_CONV REAL_POLY_CLAUSES REAL_POLY_NEG_CLAUSES
(is_ratconst,
REAL_RAT_ADD_CONV,REAL_RAT_MUL_CONV,REAL_RAT_POW_CONV)
(<);;
val ( REAL_POLY_NEG_CONV ) : term -> thm =
val ( REAL_POLY_ADD_CONV ) : term -> thm =
val ( REAL_POLY_SUB_CONV ) : term -> thm =
val ( REAL_POLY_MUL_CONV ) : term -> thm =
val ( REAL_POLY_POW_CONV ) : term -> thm =
val ( REAL_POLY_CONV ) : term -> thm =
For examples of the resulting main function in action, see