import
import_segment "hol4"
def_maps
"sums" > "sums_def"
"summable" > "summable_def"
"suminf" > "suminf_def"
"subseq" > "subseq_def"
"mono" > "mono_def"
"lim" > "lim_def"
"hol4-->" > "hol4-->_def"
"convergent" > "convergent_def"
"cauchy" > "cauchy_def"
const_maps
"sums" > "HOL4Real.seq.sums"
"summable" > "HOL4Real.seq.summable"
"suminf" > "HOL4Real.seq.suminf"
"subseq" > "HOL4Real.seq.subseq"
"mono" > "HOL4Real.seq.mono"
"lim" > "HOL4Real.seq.lim"
"hol4-->" > "HOL4Real.seq.hol4-->"
"convergent" > "HOL4Real.seq.convergent"
"cauchy" > "HOL4Real.seq.cauchy"
const_renames
"-->" > "hol4-->"
thm_maps
"tends_num_real" > "HOL4Real.seq.tends_num_real"
"sums_def" > "HOL4Real.seq.sums_def"
"sums" > "HOL4Real.seq.sums"
"summable_def" > "HOL4Real.seq.summable_def"
"summable" > "HOL4Real.seq.summable"
"suminf_def" > "HOL4Real.seq.suminf_def"
"suminf" > "HOL4Real.seq.suminf"
"subseq_def" > "HOL4Real.seq.subseq_def"
"subseq" > "HOL4Real.seq.subseq"
"mono_def" > "HOL4Real.seq.mono_def"
"mono" > "HOL4Real.seq.mono"
"lim_def" > "HOL4Real.seq.lim_def"
"lim" > "HOL4Real.seq.lim"
"hol4-->_def" > "HOL4Real.seq.hol4-->_def"
"convergent_def" > "HOL4Real.seq.convergent_def"
"convergent" > "HOL4Real.seq.convergent"
"cauchy_def" > "HOL4Real.seq.cauchy_def"
"cauchy" > "HOL4Real.seq.cauchy"
"SUM_UNIQ" > "HOL4Real.seq.SUM_UNIQ"
"SUM_SUMMABLE" > "HOL4Real.seq.SUM_SUMMABLE"
"SUMMABLE_SUM" > "HOL4Real.seq.SUMMABLE_SUM"
"SUBSEQ_SUC" > "HOL4Real.seq.SUBSEQ_SUC"
"SER_ZERO" > "HOL4Real.seq.SER_ZERO"
"SER_SUB" > "HOL4Real.seq.SER_SUB"
"SER_RATIO" > "HOL4Real.seq.SER_RATIO"
"SER_POS_LT_PAIR" > "HOL4Real.seq.SER_POS_LT_PAIR"
"SER_POS_LT" > "HOL4Real.seq.SER_POS_LT"
"SER_POS_LE" > "HOL4Real.seq.SER_POS_LE"
"SER_PAIR" > "HOL4Real.seq.SER_PAIR"
"SER_OFFSET" > "HOL4Real.seq.SER_OFFSET"
"SER_NEG" > "HOL4Real.seq.SER_NEG"
"SER_LE2" > "HOL4Real.seq.SER_LE2"
"SER_LE" > "HOL4Real.seq.SER_LE"
"SER_GROUP" > "HOL4Real.seq.SER_GROUP"
"SER_COMPARA" > "HOL4Real.seq.SER_COMPARA"
"SER_COMPAR" > "HOL4Real.seq.SER_COMPAR"
"SER_CMUL" > "HOL4Real.seq.SER_CMUL"
"SER_CDIV" > "HOL4Real.seq.SER_CDIV"
"SER_CAUCHY" > "HOL4Real.seq.SER_CAUCHY"
"SER_ADD" > "HOL4Real.seq.SER_ADD"
"SER_ACONV" > "HOL4Real.seq.SER_ACONV"
"SER_ABS" > "HOL4Real.seq.SER_ABS"
"SER_0" > "HOL4Real.seq.SER_0"
"SEQ_UNIQ" > "HOL4Real.seq.SEQ_UNIQ"
"SEQ_SUC" > "HOL4Real.seq.SEQ_SUC"
"SEQ_SUBLE" > "HOL4Real.seq.SEQ_SUBLE"
"SEQ_SUB" > "HOL4Real.seq.SEQ_SUB"
"SEQ_SBOUNDED" > "HOL4Real.seq.SEQ_SBOUNDED"
"SEQ_POWER_ABS" > "HOL4Real.seq.SEQ_POWER_ABS"
"SEQ_POWER" > "HOL4Real.seq.SEQ_POWER"
"SEQ_NEG_CONV" > "HOL4Real.seq.SEQ_NEG_CONV"
"SEQ_NEG_BOUNDED" > "HOL4Real.seq.SEQ_NEG_BOUNDED"
"SEQ_NEG" > "HOL4Real.seq.SEQ_NEG"
"SEQ_MUL" > "HOL4Real.seq.SEQ_MUL"
"SEQ_MONOSUB" > "HOL4Real.seq.SEQ_MONOSUB"
"SEQ_LIM" > "HOL4Real.seq.SEQ_LIM"
"SEQ_LE" > "HOL4Real.seq.SEQ_LE"
"SEQ_INV0" > "HOL4Real.seq.SEQ_INV0"
"SEQ_INV" > "HOL4Real.seq.SEQ_INV"
"SEQ_ICONV" > "HOL4Real.seq.SEQ_ICONV"
"SEQ_DIV" > "HOL4Real.seq.SEQ_DIV"
"SEQ_DIRECT" > "HOL4Real.seq.SEQ_DIRECT"
"SEQ_CONST" > "HOL4Real.seq.SEQ_CONST"
"SEQ_CBOUNDED" > "HOL4Real.seq.SEQ_CBOUNDED"
"SEQ_CAUCHY" > "HOL4Real.seq.SEQ_CAUCHY"
"SEQ_BOUNDED_2" > "HOL4Real.seq.SEQ_BOUNDED_2"
"SEQ_BOUNDED" > "HOL4Real.seq.SEQ_BOUNDED"
"SEQ_BCONV" > "HOL4Real.seq.SEQ_BCONV"
"SEQ_ADD" > "HOL4Real.seq.SEQ_ADD"
"SEQ_ABS_IMP" > "HOL4Real.seq.SEQ_ABS_IMP"
"SEQ_ABS" > "HOL4Real.seq.SEQ_ABS"
"SEQ" > "HOL4Real.seq.SEQ"
"NEST_LEMMA_UNIQ" > "HOL4Real.seq.NEST_LEMMA_UNIQ"
"NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA"
"MONO_SUC" > "HOL4Real.seq.MONO_SUC"
"MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
"GP_FINITE" > "HOL4Real.seq.GP_FINITE"
"GP" > "HOL4Real.seq.GP"
"BOLZANO_LEMMA" > "HOL4Real.seq.BOLZANO_LEMMA"
"ABS_NEG_LEMMA" > "HOL4Real.seq.ABS_NEG_LEMMA"
end