import
import_segment "hol4"
def_maps
"topology" > "topology_def"
"re_universe" > "re_universe_def"
"re_union" > "re_union_def"
"re_subset" > "re_subset_def"
"re_null" > "re_null_def"
"re_intersect" > "re_intersect_def"
"re_compl" > "re_compl_def"
"re_Union" > "re_Union_def"
"open" > "open_def"
"neigh" > "neigh_def"
"mtop" > "mtop_def"
"mr1" > "mr1_def"
"metric" > "metric_def"
"limpt" > "limpt_def"
"istopology" > "istopology_def"
"ismet" > "ismet_def"
"dist" > "dist_def"
"closed" > "closed_def"
"B" > "B_def"
type_maps
"topology" > "HOL4Real.topology.topology"
"metric" > "HOL4Real.topology.metric"
const_maps
"re_universe" > "HOL4Real.topology.re_universe"
"re_union" > "HOL4Real.topology.re_union"
"re_subset" > "HOL4Real.topology.re_subset"
"re_null" > "HOL4Real.topology.re_null"
"re_intersect" > "HOL4Real.topology.re_intersect"
"re_compl" > "HOL4Real.topology.re_compl"
"re_Union" > "HOL4Real.topology.re_Union"
"neigh" > "HOL4Real.topology.neigh"
"mtop" > "HOL4Real.topology.mtop"
"mr1" > "HOL4Real.topology.mr1"
"limpt" > "HOL4Real.topology.limpt"
"istopology" > "HOL4Real.topology.istopology"
"ismet" > "HOL4Real.topology.ismet"
"closed" > "HOL4Real.topology.closed"
"B" > "HOL4Real.topology.B"
thm_maps
"topology_tybij" > "HOL4Real.topology.topology_tybij"
"topology_TY_DEF" > "HOL4Real.topology.topology_TY_DEF"
"re_universe_def" > "HOL4Real.topology.re_universe_def"
"re_universe" > "HOL4Real.topology.re_universe"
"re_union_def" > "HOL4Real.topology.re_union_def"
"re_union" > "HOL4Real.topology.re_union"
"re_subset_def" > "HOL4Real.topology.re_subset_def"
"re_subset" > "HOL4Real.topology.re_subset"
"re_null_def" > "HOL4Real.topology.re_null_def"
"re_null" > "HOL4Real.topology.re_null"
"re_intersect_def" > "HOL4Real.topology.re_intersect_def"
"re_intersect" > "HOL4Real.topology.re_intersect"
"re_compl_def" > "HOL4Real.topology.re_compl_def"
"re_compl" > "HOL4Real.topology.re_compl"
"re_Union_def" > "HOL4Real.topology.re_Union_def"
"re_Union" > "HOL4Real.topology.re_Union"
"neigh_def" > "HOL4Real.topology.neigh_def"
"neigh" > "HOL4Real.topology.neigh"
"mtop_istopology" > "HOL4Real.topology.mtop_istopology"
"mtop_def" > "HOL4Real.topology.mtop_def"
"mtop" > "HOL4Real.topology.mtop"
"mr1_def" > "HOL4Real.topology.mr1_def"
"mr1" > "HOL4Real.topology.mr1"
"metric_tybij" > "HOL4Real.topology.metric_tybij"
"metric_TY_DEF" > "HOL4Real.topology.metric_TY_DEF"
"limpt_def" > "HOL4Real.topology.limpt_def"
"limpt" > "HOL4Real.topology.limpt"
"istopology_def" > "HOL4Real.topology.istopology_def"
"istopology" > "HOL4Real.topology.istopology"
"ismet_def" > "HOL4Real.topology.ismet_def"
"ismet" > "HOL4Real.topology.ismet"
"closed_def" > "HOL4Real.topology.closed_def"
"closed" > "HOL4Real.topology.closed"
"ball" > "HOL4Real.topology.ball"
"TOPOLOGY_UNION" > "HOL4Real.topology.TOPOLOGY_UNION"
"TOPOLOGY" > "HOL4Real.topology.TOPOLOGY"
"SUBSET_TRANS" > "HOL4Real.topology.SUBSET_TRANS"
"SUBSET_REFL" > "HOL4Real.topology.SUBSET_REFL"
"SUBSET_ANTISYM" > "HOL4Real.topology.SUBSET_ANTISYM"
"OPEN_UNOPEN" > "HOL4Real.topology.OPEN_UNOPEN"
"OPEN_SUBOPEN" > "HOL4Real.topology.OPEN_SUBOPEN"
"OPEN_OWN_NEIGH" > "HOL4Real.topology.OPEN_OWN_NEIGH"
"OPEN_NEIGH" > "HOL4Real.topology.OPEN_NEIGH"
"MTOP_OPEN" > "HOL4Real.topology.MTOP_OPEN"
"MTOP_LIMPT" > "HOL4Real.topology.MTOP_LIMPT"
"MR1_SUB_LT" > "HOL4Real.topology.MR1_SUB_LT"
"MR1_SUB_LE" > "HOL4Real.topology.MR1_SUB_LE"
"MR1_SUB" > "HOL4Real.topology.MR1_SUB"
"MR1_LIMPT" > "HOL4Real.topology.MR1_LIMPT"
"MR1_DEF" > "HOL4Real.topology.MR1_DEF"
"MR1_BETWEEN1" > "HOL4Real.topology.MR1_BETWEEN1"
"MR1_ADD_POS" > "HOL4Real.topology.MR1_ADD_POS"
"MR1_ADD_LT" > "HOL4Real.topology.MR1_ADD_LT"
"MR1_ADD" > "HOL4Real.topology.MR1_ADD"
"METRIC_ZERO" > "HOL4Real.topology.METRIC_ZERO"
"METRIC_TRIANGLE" > "HOL4Real.topology.METRIC_TRIANGLE"
"METRIC_SYM" > "HOL4Real.topology.METRIC_SYM"
"METRIC_SAME" > "HOL4Real.topology.METRIC_SAME"
"METRIC_POS" > "HOL4Real.topology.METRIC_POS"
"METRIC_NZ" > "HOL4Real.topology.METRIC_NZ"
"METRIC_ISMET" > "HOL4Real.topology.METRIC_ISMET"
"ISMET_R1" > "HOL4Real.topology.ISMET_R1"
"COMPL_MEM" > "HOL4Real.topology.COMPL_MEM"
"CLOSED_LIMPT" > "HOL4Real.topology.CLOSED_LIMPT"
"B_def" > "HOL4Real.topology.B_def"
"BALL_OPEN" > "HOL4Real.topology.BALL_OPEN"
"BALL_NEIGH" > "HOL4Real.topology.BALL_NEIGH"
end