import
import_segment "hol4"
def_maps
"measurable" > "measurable_primdef"
"algebra_embed" > "algebra_embed_primdef"
"alg_embed" > "alg_embed_primdef"
const_maps
"measurable" > "HOL4Prob.prob_algebra.measurable"
thm_maps
"measurable_primdef" > "HOL4Prob.prob_algebra.measurable_primdef"
"measurable_def" > "HOL4Prob.prob_algebra.measurable_def"
"algebra_embed_def" > "HOL4Prob.prob_algebra.algebra_embed_def"
"alg_embed_def" > "HOL4Prob.prob_algebra.alg_embed_def"
"MEASURABLE_UNION" > "HOL4Prob.prob_algebra.MEASURABLE_UNION"
"MEASURABLE_STL" > "HOL4Prob.prob_algebra.MEASURABLE_STL"
"MEASURABLE_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_SHD"
"MEASURABLE_SDROP" > "HOL4Prob.prob_algebra.MEASURABLE_SDROP"
"MEASURABLE_INTER_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_SHD"
"MEASURABLE_INTER_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_HALVES"
"MEASURABLE_INTER" > "HOL4Prob.prob_algebra.MEASURABLE_INTER"
"MEASURABLE_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_HALVES"
"MEASURABLE_COMPL" > "HOL4Prob.prob_algebra.MEASURABLE_COMPL"
"MEASURABLE_BASIC" > "HOL4Prob.prob_algebra.MEASURABLE_BASIC"
"MEASURABLE_ALGEBRA" > "HOL4Prob.prob_algebra.MEASURABLE_ALGEBRA"
"INTER_STL" > "HOL4Prob.prob_algebra.INTER_STL"
"HALVES_INTER" > "HOL4Prob.prob_algebra.HALVES_INTER"
"COMPL_SHD" > "HOL4Prob.prob_algebra.COMPL_SHD"
"ALG_EMBED_TWINS" > "HOL4Prob.prob_algebra.ALG_EMBED_TWINS"
"ALG_EMBED_PREFIX_SUBSET" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX_SUBSET"
"ALG_EMBED_PREFIX" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX"
"ALG_EMBED_POPULATED" > "HOL4Prob.prob_algebra.ALG_EMBED_POPULATED"
"ALG_EMBED_NIL" > "HOL4Prob.prob_algebra.ALG_EMBED_NIL"
"ALG_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALG_EMBED_BASIC"
"ALG_CANON_REP" > "HOL4Prob.prob_algebra.ALG_CANON_REP"
"ALG_CANON_PREFS_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_PREFS_EMBED"
"ALG_CANON_MERGE_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_MERGE_EMBED"
"ALG_CANON_FIND_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_FIND_EMBED"
"ALG_CANON_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_EMBED"
"ALG_CANON2_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON2_EMBED"
"ALG_CANON1_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON1_EMBED"
"ALGEBRA_EMBED_TLS" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_TLS"
"ALGEBRA_EMBED_MEM" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_MEM"
"ALGEBRA_EMBED_COMPL" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_COMPL"
"ALGEBRA_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_BASIC"
"ALGEBRA_EMBED_APPEND" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_APPEND"
"ALGEBRA_CANON_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_UNIV"
"ALGEBRA_CANON_EMBED_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_UNIV"
"ALGEBRA_CANON_EMBED_EMPTY" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_EMPTY"
end