Updated import configuration.
import
import_segment "hol4"
def_maps
"inf" > "inf_primdef"
const_maps
"inf" > "HOL4Prob.prob_extra.inf"
"COMPL" > "HOL4Base.pred_set.COMPL"
thm_maps
"inf_primdef" > "HOL4Prob.prob_extra.inf_primdef"
"inf_def" > "HOL4Prob.prob_extra.inf_def"
"X_HALF_HALF" > "HOL4Prob.prob_extra.X_HALF_HALF"
"UNION_DISJOINT_SPLIT" > "HOL4Prob.prob_extra.UNION_DISJOINT_SPLIT"
"UNION_DEF_ALT" > "HOL4Prob.prob_extra.UNION_DEF_ALT"
"SUBSET_EQ_DECOMP" > "HOL4Base.pred_set.SUBSET_ANTISYM"
"SUBSET_EQ" > "HOL4Prob.prob_extra.SUBSET_EQ"
"SET_EQ_EXT" > "HOL4Base.pred_set.EXTENSION"
"REAL_X_LE_SUP" > "HOL4Prob.prob_extra.REAL_X_LE_SUP"
"REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX"
"REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X"
"REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE"
"REAL_POW" > "RealPow.realpow_real_of_nat"
"REAL_LE_INV_LE" > "Ring_and_Field.le_imp_inverse_le"
"REAL_LE_EQ" > "Set.basic_trans_rules_26"
"REAL_INVINV_ALL" > "Ring_and_Field.inverse_inverse_eq"
"REAL_INF_MIN" > "HOL4Prob.prob_extra.REAL_INF_MIN"
"RAND_THM" > "HOL.arg_cong"
"POW_HALF_TWICE" > "HOL4Prob.prob_extra.POW_HALF_TWICE"
"POW_HALF_POS" > "HOL4Prob.prob_extra.POW_HALF_POS"
"POW_HALF_MONO" > "HOL4Prob.prob_extra.POW_HALF_MONO"
"POW_HALF_EXP" > "HOL4Prob.prob_extra.POW_HALF_EXP"
"ONE_MINUS_HALF" > "HOL4Prob.prob_extra.ONE_MINUS_HALF"
"MOD_TWO" > "HOL4Prob.prob_extra.MOD_TWO"
"MEM_NIL_MAP_CONS" > "HOL4Prob.prob_extra.MEM_NIL_MAP_CONS"
"MEM_NIL" > "HOL4Prob.prob_extra.MEM_NIL"
"MEM_FILTER" > "HOL4Prob.prob_extra.MEM_FILTER"
"MAP_MEM" > "HOL4Prob.prob_extra.MAP_MEM"
"MAP_ID" > "List.map_ident"
"LENGTH_FILTER" > "List.length_filter_le"
"LAST_MEM" > "HOL4Prob.prob_extra.LAST_MEM"
"LAST_MAP_CONS" > "HOL4Prob.prob_extra.LAST_MAP_CONS"
"IS_PREFIX_TRANS" > "HOL4Prob.prob_extra.IS_PREFIX_TRANS"
"IS_PREFIX_SNOC" > "HOL4Prob.prob_extra.IS_PREFIX_SNOC"
"IS_PREFIX_REFL" > "HOL4Prob.prob_extra.IS_PREFIX_REFL"
"IS_PREFIX_NIL" > "HOL4Prob.prob_extra.IS_PREFIX_NIL"
"IS_PREFIX_LENGTH_ANTI" > "HOL4Prob.prob_extra.IS_PREFIX_LENGTH_ANTI"
"IS_PREFIX_LENGTH" > "HOL4Prob.prob_extra.IS_PREFIX_LENGTH"
"IS_PREFIX_BUTLAST" > "HOL4Prob.prob_extra.IS_PREFIX_BUTLAST"
"IS_PREFIX_ANTISYM" > "HOL4Prob.prob_extra.IS_PREFIX_ANTISYM"
"IN_EMPTY" > "HOL4Base.pred_set.NOT_IN_EMPTY"
"IN_COMPL" > "HOL4Base.pred_set.IN_COMPL"
"INV_SUC_POS" > "HOL4Prob.prob_extra.INV_SUC_POS"
"INV_SUC_MAX" > "HOL4Prob.prob_extra.INV_SUC_MAX"
"INV_SUC" > "HOL4Prob.prob_extra.INV_SUC"
"INTER_UNION_RDISTRIB" > "HOL4Prob.prob_extra.INTER_UNION_RDISTRIB"
"INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
"INTER_IS_EMPTY" > "HOL4Prob.prob_extra.INTER_IS_EMPTY"
"INF_DEF_ALT" > "HOL4Prob.prob_extra.INF_DEF_ALT"
"HALF_POS" > "HOL4Prob.prob_extra.HALF_POS"
"HALF_LT_1" > "HOL4Prob.prob_extra.HALF_LT_1"
"HALF_CANCEL" > "HOL4Prob.prob_extra.HALF_CANCEL"
"GSPEC_DEF_ALT" > "HOL4Prob.prob_extra.GSPEC_DEF_ALT"
"FOLDR_MAP" > "HOL4Prob.prob_extra.FOLDR_MAP"
"FILTER_TRUE" > "HOL4Prob.prob_extra.FILTER_TRUE"
"FILTER_OUT_ELT" > "HOL4Prob.prob_extra.FILTER_OUT_ELT"
"FILTER_MEM" > "HOL4Prob.prob_extra.FILTER_MEM"
"FILTER_FALSE" > "HOL4Prob.prob_extra.FILTER_FALSE"
"EXP_DIV_TWO" > "HOL4Prob.prob_extra.EXP_DIV_TWO"
"EXISTS_LONGEST" > "HOL4Prob.prob_extra.EXISTS_LONGEST"
"EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ"
"EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC"
"EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO"
"EQ_EXT_EQ" > "Fun.expand_fun_eq"
"DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE"
"DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN"
"DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO"
"DIV_TWO_EXP" > "HOL4Prob.prob_extra.DIV_TWO_EXP"
"DIV_TWO_CANCEL" > "HOL4Prob.prob_extra.DIV_TWO_CANCEL"
"DIV_TWO_BASIC" > "HOL4Prob.prob_extra.DIV_TWO_BASIC"
"DIV_TWO" > "HOL4Prob.prob_extra.DIV_TWO"
"DIV_THEN_MULT" > "HOL4Prob.prob_extra.DIV_THEN_MULT"
"DIVISION_TWO" > "HOL4Prob.prob_extra.DIVISION_TWO"
"COMPL_def" > "HOL4Base.pred_set.COMPL_DEF"
"COMPL_SPLITS" > "HOL4Base.pred_set.COMPL_SPLITS"
"COMPL_COMPL" > "HOL4Base.pred_set.COMPL_COMPL"
"COMPL_CLAUSES" > "HOL4Base.pred_set.COMPL_CLAUSES"
"BOOL_BOOL_CASES_THM" > "HOL4Prob.prob_extra.BOOL_BOOL_CASES_THM"
"BOOL_BOOL_CASES" > "HOL4Base.bool.BOOL_FUN_INDUCT"
"APPEND_MEM" > "HOL4Base.list.MEM_APPEND"
"ABS_UNIT_INTERVAL" > "HOL4Prob.prob_extra.ABS_UNIT_INTERVAL"
"ABS_BETWEEN_LE" > "HOL4Prob.prob_extra.ABS_BETWEEN_LE"
end