import
import_segment "hol4"
def_maps
"indep_set" > "indep_set_primdef"
"indep" > "indep_primdef"
"alg_cover_set" > "alg_cover_set_primdef"
"alg_cover" > "alg_cover_primdef"
const_maps
"indep_set" > "HOL4Prob.prob_indep.indep_set"
"indep" > "HOL4Prob.prob_indep.indep"
"alg_cover_set" > "HOL4Prob.prob_indep.alg_cover_set"
"alg_cover" > "HOL4Prob.prob_indep.alg_cover"
thm_maps
"indep_set_primdef" > "HOL4Prob.prob_indep.indep_set_primdef"
"indep_set_def" > "HOL4Prob.prob_indep.indep_set_def"
"indep_primdef" > "HOL4Prob.prob_indep.indep_primdef"
"indep_def" > "HOL4Prob.prob_indep.indep_def"
"alg_cover_set_primdef" > "HOL4Prob.prob_indep.alg_cover_set_primdef"
"alg_cover_set_def" > "HOL4Prob.prob_indep.alg_cover_set_def"
"alg_cover_primdef" > "HOL4Prob.prob_indep.alg_cover_primdef"
"alg_cover_def" > "HOL4Prob.prob_indep.alg_cover_def"
"PROB_INDEP_BOUND" > "HOL4Prob.prob_indep.PROB_INDEP_BOUND"
"MAP_CONS_TL_FILTER" > "HOL4Prob.prob_indep.MAP_CONS_TL_FILTER"
"INDEP_UNIT" > "HOL4Prob.prob_indep.INDEP_UNIT"
"INDEP_SET_SYM" > "HOL4Prob.prob_indep.INDEP_SET_SYM"
"INDEP_SET_LIST" > "HOL4Prob.prob_indep.INDEP_SET_LIST"
"INDEP_SET_DISJOINT_DECOMP" > "HOL4Prob.prob_indep.INDEP_SET_DISJOINT_DECOMP"
"INDEP_SET_BASIC" > "HOL4Prob.prob_indep.INDEP_SET_BASIC"
"INDEP_SDEST" > "HOL4Prob.prob_indep.INDEP_SDEST"
"INDEP_PROB" > "HOL4Prob.prob_indep.INDEP_PROB"
"INDEP_MEASURABLE2" > "HOL4Prob.prob_indep.INDEP_MEASURABLE2"
"INDEP_MEASURABLE1" > "HOL4Prob.prob_indep.INDEP_MEASURABLE1"
"INDEP_INDEP_SET_LEMMA" > "HOL4Prob.prob_indep.INDEP_INDEP_SET_LEMMA"
"INDEP_INDEP_SET" > "HOL4Prob.prob_indep.INDEP_INDEP_SET"
"INDEP_BIND_SDEST" > "HOL4Prob.prob_indep.INDEP_BIND_SDEST"
"INDEP_BIND" > "HOL4Prob.prob_indep.INDEP_BIND"
"BIND_STEP" > "HOL4Prob.prob_indep.BIND_STEP"
"ALG_COVER_WELL_DEFINED" > "HOL4Prob.prob_indep.ALG_COVER_WELL_DEFINED"
"ALG_COVER_UNIV" > "HOL4Prob.prob_indep.ALG_COVER_UNIV"
"ALG_COVER_UNIQUE" > "HOL4Prob.prob_indep.ALG_COVER_UNIQUE"
"ALG_COVER_TAIL_STEP" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_STEP"
"ALG_COVER_TAIL_PROB" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_PROB"
"ALG_COVER_TAIL_MEASURABLE" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_MEASURABLE"
"ALG_COVER_STEP" > "HOL4Prob.prob_indep.ALG_COVER_STEP"
"ALG_COVER_SET_INDUCTION" > "HOL4Prob.prob_indep.ALG_COVER_SET_INDUCTION"
"ALG_COVER_SET_CASES_THM" > "HOL4Prob.prob_indep.ALG_COVER_SET_CASES_THM"
"ALG_COVER_SET_CASES" > "HOL4Prob.prob_indep.ALG_COVER_SET_CASES"
"ALG_COVER_SET_BASIC" > "HOL4Prob.prob_indep.ALG_COVER_SET_BASIC"
"ALG_COVER_HEAD" > "HOL4Prob.prob_indep.ALG_COVER_HEAD"
"ALG_COVER_EXISTS_UNIQUE" > "HOL4Prob.prob_indep.ALG_COVER_EXISTS_UNIQUE"
end