import
import_segment "hol4"
def_maps
"tends_real_real" > "tends_real_real_def"
"diffl" > "diffl_def"
"differentiable" > "differentiable_def"
"contl" > "contl_def"
const_maps
"tends_real_real" > "HOL4Real.lim.tends_real_real"
"diffl" > "HOL4Real.lim.diffl"
"differentiable" > "HOL4Real.lim.differentiable"
"contl" > "HOL4Real.lim.contl"
thm_maps
"tends_real_real_def" > "HOL4Real.lim.tends_real_real_def"
"tends_real_real" > "HOL4Real.lim.tends_real_real"
"diffl_def" > "HOL4Real.lim.diffl_def"
"diffl" > "HOL4Real.lim.diffl"
"differentiable_def" > "HOL4Real.lim.differentiable_def"
"differentiable" > "HOL4Real.lim.differentiable"
"contl_def" > "HOL4Real.lim.contl_def"
"contl" > "HOL4Real.lim.contl"
"ROLLE" > "HOL4Real.lim.ROLLE"
"MVT_LEMMA" > "HOL4Real.lim.MVT_LEMMA"
"MVT" > "HOL4Real.lim.MVT"
"LIM_X" > "HOL4Real.lim.LIM_X"
"LIM_UNIQ" > "HOL4Real.lim.LIM_UNIQ"
"LIM_TRANSFORM" > "HOL4Real.lim.LIM_TRANSFORM"
"LIM_SUB" > "HOL4Real.lim.LIM_SUB"
"LIM_NULL" > "HOL4Real.lim.LIM_NULL"
"LIM_NEG" > "HOL4Real.lim.LIM_NEG"
"LIM_MUL" > "HOL4Real.lim.LIM_MUL"
"LIM_INV" > "HOL4Real.lim.LIM_INV"
"LIM_EQUAL" > "HOL4Real.lim.LIM_EQUAL"
"LIM_DIV" > "HOL4Real.lim.LIM_DIV"
"LIM_CONST" > "HOL4Real.lim.LIM_CONST"
"LIM_ADD" > "HOL4Real.lim.LIM_ADD"
"LIM" > "HOL4Real.lim.LIM"
"IVT2" > "HOL4Real.lim.IVT2"
"IVT" > "HOL4Real.lim.IVT"
"INTERVAL_LEMMA" > "HOL4Real.lim.INTERVAL_LEMMA"
"INTERVAL_CLEMMA" > "HOL4Real.lim.INTERVAL_CLEMMA"
"INTERVAL_ABS" > "HOL4Real.lim.INTERVAL_ABS"
"DIFF_XM1" > "HOL4Real.lim.DIFF_XM1"
"DIFF_X" > "HOL4Real.lim.DIFF_X"
"DIFF_UNIQ" > "HOL4Real.lim.DIFF_UNIQ"
"DIFF_SUM" > "HOL4Real.lim.DIFF_SUM"
"DIFF_SUB" > "HOL4Real.lim.DIFF_SUB"
"DIFF_POW" > "HOL4Real.lim.DIFF_POW"
"DIFF_NEG" > "HOL4Real.lim.DIFF_NEG"
"DIFF_MUL" > "HOL4Real.lim.DIFF_MUL"
"DIFF_LMIN" > "HOL4Real.lim.DIFF_LMIN"
"DIFF_LMAX" > "HOL4Real.lim.DIFF_LMAX"
"DIFF_LINC" > "HOL4Real.lim.DIFF_LINC"
"DIFF_LDEC" > "HOL4Real.lim.DIFF_LDEC"
"DIFF_LCONST" > "HOL4Real.lim.DIFF_LCONST"
"DIFF_ISCONST_END" > "HOL4Real.lim.DIFF_ISCONST_END"
"DIFF_ISCONST_ALL" > "HOL4Real.lim.DIFF_ISCONST_ALL"
"DIFF_ISCONST" > "HOL4Real.lim.DIFF_ISCONST"
"DIFF_INVERSE_OPEN" > "HOL4Real.lim.DIFF_INVERSE_OPEN"
"DIFF_INVERSE_LT" > "HOL4Real.lim.DIFF_INVERSE_LT"
"DIFF_INVERSE" > "HOL4Real.lim.DIFF_INVERSE"
"DIFF_INV" > "HOL4Real.lim.DIFF_INV"
"DIFF_DIV" > "HOL4Real.lim.DIFF_DIV"
"DIFF_CONT" > "HOL4Real.lim.DIFF_CONT"
"DIFF_CONST" > "HOL4Real.lim.DIFF_CONST"
"DIFF_CMUL" > "HOL4Real.lim.DIFF_CMUL"
"DIFF_CHAIN" > "HOL4Real.lim.DIFF_CHAIN"
"DIFF_CARAT" > "HOL4Real.lim.DIFF_CARAT"
"DIFF_ADD" > "HOL4Real.lim.DIFF_ADD"
"CONT_SUB" > "HOL4Real.lim.CONT_SUB"
"CONT_NEG" > "HOL4Real.lim.CONT_NEG"
"CONT_MUL" > "HOL4Real.lim.CONT_MUL"
"CONT_INVERSE" > "HOL4Real.lim.CONT_INVERSE"
"CONT_INV" > "HOL4Real.lim.CONT_INV"
"CONT_INJ_RANGE" > "HOL4Real.lim.CONT_INJ_RANGE"
"CONT_INJ_LEMMA2" > "HOL4Real.lim.CONT_INJ_LEMMA2"
"CONT_INJ_LEMMA" > "HOL4Real.lim.CONT_INJ_LEMMA"
"CONT_HASSUP" > "HOL4Real.lim.CONT_HASSUP"
"CONT_DIV" > "HOL4Real.lim.CONT_DIV"
"CONT_CONST" > "HOL4Real.lim.CONT_CONST"
"CONT_COMPOSE" > "HOL4Real.lim.CONT_COMPOSE"
"CONT_BOUNDED" > "HOL4Real.lim.CONT_BOUNDED"
"CONT_ATTAINS_ALL" > "HOL4Real.lim.CONT_ATTAINS_ALL"
"CONT_ATTAINS2" > "HOL4Real.lim.CONT_ATTAINS2"
"CONT_ATTAINS" > "HOL4Real.lim.CONT_ATTAINS"
"CONT_ADD" > "HOL4Real.lim.CONT_ADD"
"CONTL_LIM" > "HOL4Real.lim.CONTL_LIM"
end