import
import_segment "hol4"
def_maps
"tendsto" > "tendsto_def"
"tends" > "tends_def"
"dorder" > "dorder_def"
"bounded" > "bounded_def"
const_maps
"tendsto" > "HOL4Real.nets.tendsto"
"tends" > "HOL4Real.nets.tends"
"dorder" > "HOL4Real.nets.dorder"
"bounded" > "HOL4Real.nets.bounded"
thm_maps
"tendsto_def" > "HOL4Real.nets.tendsto_def"
"tendsto" > "HOL4Real.nets.tendsto"
"tends_def" > "HOL4Real.nets.tends_def"
"tends" > "HOL4Real.nets.tends"
"dorder_def" > "HOL4Real.nets.dorder_def"
"dorder" > "HOL4Real.nets.dorder"
"bounded_def" > "HOL4Real.nets.bounded_def"
"bounded" > "HOL4Real.nets.bounded"
"SEQ_TENDS" > "HOL4Real.nets.SEQ_TENDS"
"NET_SUB" > "HOL4Real.nets.NET_SUB"
"NET_NULL_MUL" > "HOL4Real.nets.NET_NULL_MUL"
"NET_NULL_CMUL" > "HOL4Real.nets.NET_NULL_CMUL"
"NET_NULL_ADD" > "HOL4Real.nets.NET_NULL_ADD"
"NET_NULL" > "HOL4Real.nets.NET_NULL"
"NET_NEG" > "HOL4Real.nets.NET_NEG"
"NET_MUL" > "HOL4Real.nets.NET_MUL"
"NET_LE" > "HOL4Real.nets.NET_LE"
"NET_INV" > "HOL4Real.nets.NET_INV"
"NET_DIV" > "HOL4Real.nets.NET_DIV"
"NET_CONV_NZ" > "HOL4Real.nets.NET_CONV_NZ"
"NET_CONV_IBOUNDED" > "HOL4Real.nets.NET_CONV_IBOUNDED"
"NET_CONV_BOUNDED" > "HOL4Real.nets.NET_CONV_BOUNDED"
"NET_ADD" > "HOL4Real.nets.NET_ADD"
"NET_ABS" > "HOL4Real.nets.NET_ABS"
"MTOP_TENDS_UNIQ" > "HOL4Real.nets.MTOP_TENDS_UNIQ"
"MTOP_TENDS" > "HOL4Real.nets.MTOP_TENDS"
"MR1_BOUNDED" > "HOL4Real.nets.MR1_BOUNDED"
"LIM_TENDS2" > "HOL4Real.nets.LIM_TENDS2"
"LIM_TENDS" > "HOL4Real.nets.LIM_TENDS"
"DORDER_TENDSTO" > "HOL4Real.nets.DORDER_TENDSTO"
"DORDER_NGE" > "HOL4Real.nets.DORDER_NGE"
"DORDER_LEMMA" > "HOL4Real.nets.DORDER_LEMMA"
end