import
import_segment "hol4"
def_maps
"prob" > "prob_primdef"
"algebra_measure" > "algebra_measure_primdef"
"alg_measure" > "alg_measure_primdef"
const_maps
"prob" > "HOL4Prob.prob.prob"
"algebra_measure" > "HOL4Prob.prob.algebra_measure"
thm_maps
"prob_primdef" > "HOL4Prob.prob.prob_primdef"
"prob_def" > "HOL4Prob.prob.prob_def"
"algebra_measure_primdef" > "HOL4Prob.prob.algebra_measure_primdef"
"algebra_measure_def" > "HOL4Prob.prob.algebra_measure_def"
"alg_measure_def" > "HOL4Prob.prob.alg_measure_def"
"X_LE_PROB" > "HOL4Prob.prob.X_LE_PROB"
"PROB_SUP_EXISTS2" > "HOL4Prob.prob.PROB_SUP_EXISTS2"
"PROB_SUP_EXISTS1" > "HOL4Prob.prob.PROB_SUP_EXISTS1"
"PROB_SUBSET_MONO" > "HOL4Prob.prob.PROB_SUBSET_MONO"
"PROB_STL" > "HOL4Prob.prob.PROB_STL"
"PROB_SHD" > "HOL4Prob.prob.PROB_SHD"
"PROB_SDROP" > "HOL4Prob.prob.PROB_SDROP"
"PROB_RANGE" > "HOL4Prob.prob.PROB_RANGE"
"PROB_POS" > "HOL4Prob.prob.PROB_POS"
"PROB_MAX" > "HOL4Prob.prob.PROB_MAX"
"PROB_LE_X" > "HOL4Prob.prob.PROB_LE_X"
"PROB_INTER_SHD" > "HOL4Prob.prob.PROB_INTER_SHD"
"PROB_INTER_HALVES" > "HOL4Prob.prob.PROB_INTER_HALVES"
"PROB_COMPL_LE1" > "HOL4Prob.prob.PROB_COMPL_LE1"
"PROB_COMPL" > "HOL4Prob.prob.PROB_COMPL"
"PROB_BASIC" > "HOL4Prob.prob.PROB_BASIC"
"PROB_ALGEBRA" > "HOL4Prob.prob.PROB_ALGEBRA"
"PROB_ALG" > "HOL4Prob.prob.PROB_ALG"
"PROB_ADDITIVE" > "HOL4Prob.prob.PROB_ADDITIVE"
"ALG_TWINS_MEASURE" > "HOL4Prob.prob.ALG_TWINS_MEASURE"
"ALG_MEASURE_TLS" > "HOL4Prob.prob.ALG_MEASURE_TLS"
"ALG_MEASURE_POS" > "HOL4Prob.prob.ALG_MEASURE_POS"
"ALG_MEASURE_COMPL" > "HOL4Prob.prob.ALG_MEASURE_COMPL"
"ALG_MEASURE_BASIC" > "HOL4Prob.prob.ALG_MEASURE_BASIC"
"ALG_MEASURE_APPEND" > "HOL4Prob.prob.ALG_MEASURE_APPEND"
"ALG_MEASURE_ADDITIVE" > "HOL4Prob.prob.ALG_MEASURE_ADDITIVE"
"ALG_CANON_PREFS_MONO" > "HOL4Prob.prob.ALG_CANON_PREFS_MONO"
"ALG_CANON_MONO" > "HOL4Prob.prob.ALG_CANON_MONO"
"ALG_CANON_MERGE_MONO" > "HOL4Prob.prob.ALG_CANON_MERGE_MONO"
"ALG_CANON_FIND_MONO" > "HOL4Prob.prob.ALG_CANON_FIND_MONO"
"ALG_CANON2_MONO" > "HOL4Prob.prob.ALG_CANON2_MONO"
"ALG_CANON1_MONO" > "HOL4Prob.prob.ALG_CANON1_MONO"
"ALGEBRA_MEASURE_RANGE" > "HOL4Prob.prob.ALGEBRA_MEASURE_RANGE"
"ALGEBRA_MEASURE_POS" > "HOL4Prob.prob.ALGEBRA_MEASURE_POS"
"ALGEBRA_MEASURE_MONO_EMBED" > "HOL4Prob.prob.ALGEBRA_MEASURE_MONO_EMBED"
"ALGEBRA_MEASURE_MAX" > "HOL4Prob.prob.ALGEBRA_MEASURE_MAX"
"ALGEBRA_MEASURE_DEF_ALT" > "HOL4Prob.prob.ALGEBRA_MEASURE_DEF_ALT"
"ALGEBRA_MEASURE_BASIC" > "HOL4Prob.prob.ALGEBRA_MEASURE_BASIC"
"ALGEBRA_CANON_MEASURE_MAX" > "HOL4Prob.prob.ALGEBRA_CANON_MEASURE_MAX"
"ABS_PROB" > "HOL4Prob.prob.ABS_PROB"
end