import
import_segment "hol4"
def_maps
"rsquarefree" > "rsquarefree_def"
"poly_order" > "poly_order_def"
"poly_neg" > "poly_neg_primdef"
"poly_mul" > "poly_mul_primdef"
"poly_exp" > "poly_exp_primdef"
"poly_divides" > "poly_divides_def"
"poly_diff_aux" > "poly_diff_aux_primdef"
"poly_add" > "poly_add_primdef"
"poly" > "poly_primdef"
"normalize" > "normalize_def"
"diff" > "diff_def"
"degree" > "degree_def"
"##" > "##_def"
const_maps
"rsquarefree" > "HOL4Real.poly.rsquarefree"
"poly_order" > "HOL4Real.poly.poly_order"
"poly_neg" > "HOL4Real.poly.poly_neg"
"poly_divides" > "HOL4Real.poly.poly_divides"
"diff" > "HOL4Real.poly.diff"
"degree" > "HOL4Real.poly.degree"
thm_maps
"rsquarefree_def" > "HOL4Real.poly.rsquarefree_def"
"rsquarefree" > "HOL4Real.poly.rsquarefree"
"poly_order_def" > "HOL4Real.poly.poly_order_def"
"poly_order" > "HOL4Real.poly.poly_order"
"poly_neg_primdef" > "HOL4Real.poly.poly_neg_primdef"
"poly_neg_def" > "HOL4Real.poly.poly_neg_def"
"poly_mul_def" > "HOL4Real.poly.poly_mul_def"
"poly_exp_def" > "HOL4Real.poly.poly_exp_def"
"poly_divides_def" > "HOL4Real.poly.poly_divides_def"
"poly_divides" > "HOL4Real.poly.poly_divides"
"poly_diff_def" > "HOL4Real.poly.poly_diff_def"
"poly_diff_aux_def" > "HOL4Real.poly.poly_diff_aux_def"
"poly_def" > "HOL4Real.poly.poly_def"
"poly_cmul_def" > "HOL4Real.poly.poly_cmul_def"
"poly_add_def" > "HOL4Real.poly.poly_add_def"
"normalize" > "HOL4Real.poly.normalize"
"diff_def" > "HOL4Real.poly.diff_def"
"degree_def" > "HOL4Real.poly.degree_def"
"degree" > "HOL4Real.poly.degree"
"RSQUAREFREE_ROOTS" > "HOL4Real.poly.RSQUAREFREE_ROOTS"
"RSQUAREFREE_DECOMP" > "HOL4Real.poly.RSQUAREFREE_DECOMP"
"POLY_ZERO_LEMMA" > "HOL4Real.poly.POLY_ZERO_LEMMA"
"POLY_ZERO" > "HOL4Real.poly.POLY_ZERO"
"POLY_SQUAREFREE_DECOMP_ORDER" > "HOL4Real.poly.POLY_SQUAREFREE_DECOMP_ORDER"
"POLY_SQUAREFREE_DECOMP" > "HOL4Real.poly.POLY_SQUAREFREE_DECOMP"
"POLY_ROOTS_INDEX_LENGTH" > "HOL4Real.poly.POLY_ROOTS_INDEX_LENGTH"
"POLY_ROOTS_INDEX_LEMMA" > "HOL4Real.poly.POLY_ROOTS_INDEX_LEMMA"
"POLY_ROOTS_FINITE_SET" > "HOL4Real.poly.POLY_ROOTS_FINITE_SET"
"POLY_ROOTS_FINITE_LEMMA" > "HOL4Real.poly.POLY_ROOTS_FINITE_LEMMA"
"POLY_ROOTS_FINITE" > "HOL4Real.poly.POLY_ROOTS_FINITE"
"POLY_PRIME_EQ_0" > "HOL4Real.poly.POLY_PRIME_EQ_0"
"POLY_PRIMES" > "HOL4Real.poly.POLY_PRIMES"
"POLY_ORDER_EXISTS" > "HOL4Real.poly.POLY_ORDER_EXISTS"
"POLY_ORDER" > "HOL4Real.poly.POLY_ORDER"
"POLY_NORMALIZE" > "HOL4Real.poly.POLY_NORMALIZE"
"POLY_NEG_CLAUSES" > "HOL4Real.poly.POLY_NEG_CLAUSES"
"POLY_NEG" > "HOL4Real.poly.POLY_NEG"
"POLY_MVT" > "HOL4Real.poly.POLY_MVT"
"POLY_MUL_LCANCEL" > "HOL4Real.poly.POLY_MUL_LCANCEL"
"POLY_MUL_CLAUSES" > "HOL4Real.poly.POLY_MUL_CLAUSES"
"POLY_MUL_ASSOC" > "HOL4Real.poly.POLY_MUL_ASSOC"
"POLY_MUL" > "HOL4Real.poly.POLY_MUL"
"POLY_MONO" > "HOL4Real.poly.POLY_MONO"
"POLY_LINEAR_REM" > "HOL4Real.poly.POLY_LINEAR_REM"
"POLY_LINEAR_DIVIDES" > "HOL4Real.poly.POLY_LINEAR_DIVIDES"
"POLY_LENGTH_MUL" > "HOL4Real.poly.POLY_LENGTH_MUL"
"POLY_IVT_POS" > "HOL4Real.poly.POLY_IVT_POS"
"POLY_IVT_NEG" > "HOL4Real.poly.POLY_IVT_NEG"
"POLY_EXP_PRIME_EQ_0" > "HOL4Real.poly.POLY_EXP_PRIME_EQ_0"
"POLY_EXP_EQ_0" > "HOL4Real.poly.POLY_EXP_EQ_0"
"POLY_EXP_DIVIDES" > "HOL4Real.poly.POLY_EXP_DIVIDES"
"POLY_EXP_ADD" > "HOL4Real.poly.POLY_EXP_ADD"
"POLY_EXP" > "HOL4Real.poly.POLY_EXP"
"POLY_ENTIRE_LEMMA" > "HOL4Real.poly.POLY_ENTIRE_LEMMA"
"POLY_ENTIRE" > "HOL4Real.poly.POLY_ENTIRE"
"POLY_DIVIDES_ZERO" > "HOL4Real.poly.POLY_DIVIDES_ZERO"
"POLY_DIVIDES_TRANS" > "HOL4Real.poly.POLY_DIVIDES_TRANS"
"POLY_DIVIDES_SUB2" > "HOL4Real.poly.POLY_DIVIDES_SUB2"
"POLY_DIVIDES_SUB" > "HOL4Real.poly.POLY_DIVIDES_SUB"
"POLY_DIVIDES_REFL" > "HOL4Real.poly.POLY_DIVIDES_REFL"
"POLY_DIVIDES_EXP" > "HOL4Real.poly.POLY_DIVIDES_EXP"
"POLY_DIVIDES_ADD" > "HOL4Real.poly.POLY_DIVIDES_ADD"
"POLY_DIFF_ZERO" > "HOL4Real.poly.POLY_DIFF_ZERO"
"POLY_DIFF_WELLDEF" > "HOL4Real.poly.POLY_DIFF_WELLDEF"
"POLY_DIFF_NEG" > "HOL4Real.poly.POLY_DIFF_NEG"
"POLY_DIFF_MUL_LEMMA" > "HOL4Real.poly.POLY_DIFF_MUL_LEMMA"
"POLY_DIFF_MUL" > "HOL4Real.poly.POLY_DIFF_MUL"
"POLY_DIFF_LEMMA" > "HOL4Real.poly.POLY_DIFF_LEMMA"
"POLY_DIFF_ISZERO" > "HOL4Real.poly.POLY_DIFF_ISZERO"
"POLY_DIFF_EXP_PRIME" > "HOL4Real.poly.POLY_DIFF_EXP_PRIME"
"POLY_DIFF_EXP" > "HOL4Real.poly.POLY_DIFF_EXP"
"POLY_DIFF_CMUL" > "HOL4Real.poly.POLY_DIFF_CMUL"
"POLY_DIFF_CLAUSES" > "HOL4Real.poly.POLY_DIFF_CLAUSES"
"POLY_DIFF_AUX_NEG" > "HOL4Real.poly.POLY_DIFF_AUX_NEG"
"POLY_DIFF_AUX_MUL_LEMMA" > "HOL4Real.poly.POLY_DIFF_AUX_MUL_LEMMA"
"POLY_DIFF_AUX_ISZERO" > "HOL4Real.poly.POLY_DIFF_AUX_ISZERO"
"POLY_DIFF_AUX_CMUL" > "HOL4Real.poly.POLY_DIFF_AUX_CMUL"
"POLY_DIFF_AUX_ADD" > "HOL4Real.poly.POLY_DIFF_AUX_ADD"
"POLY_DIFF_ADD" > "HOL4Real.poly.POLY_DIFF_ADD"
"POLY_DIFFERENTIABLE" > "HOL4Real.poly.POLY_DIFFERENTIABLE"
"POLY_DIFF" > "HOL4Real.poly.POLY_DIFF"
"POLY_CONT" > "HOL4Real.poly.POLY_CONT"
"POLY_CMUL_CLAUSES" > "HOL4Real.poly.POLY_CMUL_CLAUSES"
"POLY_CMUL" > "HOL4Real.poly.POLY_CMUL"
"POLY_ADD_RZERO" > "HOL4Real.poly.POLY_ADD_RZERO"
"POLY_ADD_CLAUSES" > "HOL4Real.poly.POLY_ADD_CLAUSES"
"POLY_ADD" > "HOL4Real.poly.POLY_ADD"
"ORDER_UNIQUE" > "HOL4Real.poly.ORDER_UNIQUE"
"ORDER_THM" > "HOL4Real.poly.ORDER_THM"
"ORDER_ROOT" > "HOL4Real.poly.ORDER_ROOT"
"ORDER_POLY" > "HOL4Real.poly.ORDER_POLY"
"ORDER_MUL" > "HOL4Real.poly.ORDER_MUL"
"ORDER_DIVIDES" > "HOL4Real.poly.ORDER_DIVIDES"
"ORDER_DIFF" > "HOL4Real.poly.ORDER_DIFF"
"ORDER_DECOMP" > "HOL4Real.poly.ORDER_DECOMP"
"ORDER" > "HOL4Real.poly.ORDER"
"FINITE_LEMMA" > "HOL4Real.poly.FINITE_LEMMA"
"DEGREE_ZERO" > "HOL4Real.poly.DEGREE_ZERO"
end