import
import_segment "hol4"
def_maps
"tdiv" > "tdiv_def"
"tan" > "tan_def"
"sqrt" > "sqrt_def"
"sin" > "sin_def"
"rsum" > "rsum_def"
"root" > "root_def"
"pi" > "pi_def"
"ln" > "ln_def"
"gauge" > "gauge_def"
"fine" > "fine_def"
"exp" > "exp_def"
"dsize" > "dsize_def"
"division" > "division_def"
"cos" > "cos_def"
"atn" > "atn_def"
"asn" > "asn_def"
"acs" > "acs_def"
"Dint" > "Dint_def"
const_maps
"tdiv" > "HOL4Real.transc.tdiv"
"tan" > "HOL4Real.transc.tan"
"sqrt" > "HOL4Real.transc.sqrt"
"sin" > "HOL4Real.transc.sin"
"rsum" > "HOL4Real.transc.rsum"
"root" > "HOL4Real.transc.root"
"pi" > "HOL4Real.transc.pi"
"ln" > "HOL4Real.transc.ln"
"gauge" > "HOL4Real.transc.gauge"
"fine" > "HOL4Real.transc.fine"
"exp" > "HOL4Real.transc.exp"
"dsize" > "HOL4Real.transc.dsize"
"division" > "HOL4Real.transc.division"
"cos" > "HOL4Real.transc.cos"
"atn" > "HOL4Real.transc.atn"
"asn" > "HOL4Real.transc.asn"
"acs" > "HOL4Real.transc.acs"
"Dint" > "HOL4Real.transc.Dint"
thm_maps
"tdiv_def" > "HOL4Real.transc.tdiv_def"
"tdiv" > "HOL4Real.transc.tdiv"
"tan_def" > "HOL4Real.transc.tan_def"
"tan" > "HOL4Real.transc.tan"
"sqrt_def" > "HOL4Real.transc.sqrt_def"
"sqrt" > "HOL4Real.transc.sqrt"
"sin_def" > "HOL4Real.transc.sin_def"
"sin" > "HOL4Real.transc.sin"
"rsum_def" > "HOL4Real.transc.rsum_def"
"rsum" > "HOL4Real.transc.rsum"
"root_def" > "HOL4Real.transc.root_def"
"root" > "HOL4Real.transc.root"
"pi_def" > "HOL4Real.transc.pi_def"
"pi" > "HOL4Real.transc.pi"
"ln_def" > "HOL4Real.transc.ln_def"
"ln" > "HOL4Real.transc.ln"
"gauge_def" > "HOL4Real.transc.gauge_def"
"gauge" > "HOL4Real.transc.gauge"
"fine_def" > "HOL4Real.transc.fine_def"
"fine" > "HOL4Real.transc.fine"
"exp_def" > "HOL4Real.transc.exp_def"
"exp" > "HOL4Real.transc.exp"
"dsize_def" > "HOL4Real.transc.dsize_def"
"dsize" > "HOL4Real.transc.dsize"
"division_def" > "HOL4Real.transc.division_def"
"division" > "HOL4Real.transc.division"
"cos_def" > "HOL4Real.transc.cos_def"
"cos" > "HOL4Real.transc.cos"
"atn_def" > "HOL4Real.transc.atn_def"
"atn" > "HOL4Real.transc.atn"
"asn_def" > "HOL4Real.transc.asn_def"
"asn" > "HOL4Real.transc.asn"
"acs_def" > "HOL4Real.transc.acs_def"
"acs" > "HOL4Real.transc.acs"
"TAN_TOTAL_POS" > "HOL4Real.transc.TAN_TOTAL_POS"
"TAN_TOTAL_LEMMA" > "HOL4Real.transc.TAN_TOTAL_LEMMA"
"TAN_TOTAL" > "HOL4Real.transc.TAN_TOTAL"
"TAN_SEC" > "HOL4Real.transc.TAN_SEC"
"TAN_POS_PI2" > "HOL4Real.transc.TAN_POS_PI2"
"TAN_PI" > "HOL4Real.transc.TAN_PI"
"TAN_PERIODIC" > "HOL4Real.transc.TAN_PERIODIC"
"TAN_NPI" > "HOL4Real.transc.TAN_NPI"
"TAN_NEG" > "HOL4Real.transc.TAN_NEG"
"TAN_DOUBLE" > "HOL4Real.transc.TAN_DOUBLE"
"TAN_ATN" > "HOL4Real.transc.TAN_ATN"
"TAN_ADD" > "HOL4Real.transc.TAN_ADD"
"TAN_0" > "HOL4Real.transc.TAN_0"
"SQRT_POW_2" > "HOL4Real.transc.SQRT_POW_2"
"SQRT_POW2" > "HOL4Real.transc.SQRT_POW2"
"SQRT_POS_UNIQ" > "HOL4Real.transc.SQRT_POS_UNIQ"
"SQRT_POS_LT" > "HOL4Real.transc.SQRT_POS_LT"
"SQRT_POS_LE" > "HOL4Real.transc.SQRT_POS_LE"
"SQRT_MUL" > "HOL4Real.transc.SQRT_MUL"
"SQRT_MONO_LE" > "HOL4Real.transc.SQRT_MONO_LE"
"SQRT_INV" > "HOL4Real.transc.SQRT_INV"
"SQRT_EVEN_POW2" > "HOL4Real.transc.SQRT_EVEN_POW2"
"SQRT_EQ" > "HOL4Real.transc.SQRT_EQ"
"SQRT_DIV" > "HOL4Real.transc.SQRT_DIV"
"SQRT_1" > "HOL4Real.transc.SQRT_1"
"SQRT_0" > "HOL4Real.transc.SQRT_0"
"SIN_ZERO_LEMMA" > "HOL4Real.transc.SIN_ZERO_LEMMA"
"SIN_ZERO" > "HOL4Real.transc.SIN_ZERO"
"SIN_TOTAL" > "HOL4Real.transc.SIN_TOTAL"
"SIN_POS_PI_LE" > "HOL4Real.transc.SIN_POS_PI_LE"
"SIN_POS_PI2_LE" > "HOL4Real.transc.SIN_POS_PI2_LE"
"SIN_POS_PI2" > "HOL4Real.transc.SIN_POS_PI2"
"SIN_POS_PI" > "HOL4Real.transc.SIN_POS_PI"
"SIN_POS" > "HOL4Real.transc.SIN_POS"
"SIN_PI2" > "HOL4Real.transc.SIN_PI2"
"SIN_PI" > "HOL4Real.transc.SIN_PI"
"SIN_PERIODIC_PI" > "HOL4Real.transc.SIN_PERIODIC_PI"
"SIN_PERIODIC" > "HOL4Real.transc.SIN_PERIODIC"
"SIN_PAIRED" > "HOL4Real.transc.SIN_PAIRED"
"SIN_NPI" > "HOL4Real.transc.SIN_NPI"
"SIN_NEGLEMMA" > "HOL4Real.transc.SIN_NEGLEMMA"
"SIN_NEG" > "HOL4Real.transc.SIN_NEG"
"SIN_FDIFF" > "HOL4Real.transc.SIN_FDIFF"
"SIN_DOUBLE" > "HOL4Real.transc.SIN_DOUBLE"
"SIN_COS_SQRT" > "HOL4Real.transc.SIN_COS_SQRT"
"SIN_COS_SQ" > "HOL4Real.transc.SIN_COS_SQ"
"SIN_COS_NEG" > "HOL4Real.transc.SIN_COS_NEG"
"SIN_COS_ADD" > "HOL4Real.transc.SIN_COS_ADD"
"SIN_COS" > "HOL4Real.transc.SIN_COS"
"SIN_CONVERGES" > "HOL4Real.transc.SIN_CONVERGES"
"SIN_CIRCLE" > "HOL4Real.transc.SIN_CIRCLE"
"SIN_BOUNDS" > "HOL4Real.transc.SIN_BOUNDS"
"SIN_BOUND" > "HOL4Real.transc.SIN_BOUND"
"SIN_ASN" > "HOL4Real.transc.SIN_ASN"
"SIN_ADD" > "HOL4Real.transc.SIN_ADD"
"SIN_ACS_NZ" > "HOL4Real.transc.SIN_ACS_NZ"
"SIN_0" > "HOL4Real.transc.SIN_0"
"ROOT_POW_POS" > "HOL4Real.transc.ROOT_POW_POS"
"ROOT_POS_UNIQ" > "HOL4Real.transc.ROOT_POS_UNIQ"
"ROOT_POS_LT" > "HOL4Real.transc.ROOT_POS_LT"
"ROOT_POS" > "HOL4Real.transc.ROOT_POS"
"ROOT_MUL" > "HOL4Real.transc.ROOT_MUL"
"ROOT_MONO_LE" > "HOL4Real.transc.ROOT_MONO_LE"
"ROOT_LT_LEMMA" > "HOL4Real.transc.ROOT_LT_LEMMA"
"ROOT_LN" > "HOL4Real.transc.ROOT_LN"
"ROOT_INV" > "HOL4Real.transc.ROOT_INV"
"ROOT_DIV" > "HOL4Real.transc.ROOT_DIV"
"ROOT_1" > "HOL4Real.transc.ROOT_1"
"ROOT_0" > "HOL4Real.transc.ROOT_0"
"REAL_DIV_SQRT" > "HOL4Real.transc.REAL_DIV_SQRT"
"POW_ROOT_POS" > "HOL4Real.transc.POW_ROOT_POS"
"POW_2_SQRT" > "HOL4Real.transc.POW_2_SQRT"
"PI_POS" > "HOL4Real.transc.PI_POS"
"PI2_BOUNDS" > "HOL4Real.transc.PI2_BOUNDS"
"PI2" > "HOL4Real.transc.PI2"
"MCLAURIN_ZERO" > "HOL4Real.transc.MCLAURIN_ZERO"
"MCLAURIN_NEG" > "HOL4Real.transc.MCLAURIN_NEG"
"MCLAURIN_EXP_LT" > "HOL4Real.transc.MCLAURIN_EXP_LT"
"MCLAURIN_EXP_LE" > "HOL4Real.transc.MCLAURIN_EXP_LE"
"MCLAURIN_ALL_LT" > "HOL4Real.transc.MCLAURIN_ALL_LT"
"MCLAURIN_ALL_LE" > "HOL4Real.transc.MCLAURIN_ALL_LE"
"MCLAURIN" > "HOL4Real.transc.MCLAURIN"
"LN_POW" > "HOL4Real.transc.LN_POW"
"LN_POS" > "HOL4Real.transc.LN_POS"
"LN_MUL" > "HOL4Real.transc.LN_MUL"
"LN_MONO_LT" > "HOL4Real.transc.LN_MONO_LT"
"LN_MONO_LE" > "HOL4Real.transc.LN_MONO_LE"
"LN_LT_X" > "HOL4Real.transc.LN_LT_X"
"LN_LE" > "HOL4Real.transc.LN_LE"
"LN_INV" > "HOL4Real.transc.LN_INV"
"LN_INJ" > "HOL4Real.transc.LN_INJ"
"LN_EXP" > "HOL4Real.transc.LN_EXP"
"LN_DIV" > "HOL4Real.transc.LN_DIV"
"LN_1" > "HOL4Real.transc.LN_1"
"INTEGRAL_NULL" > "HOL4Real.transc.INTEGRAL_NULL"
"GAUGE_MIN" > "HOL4Real.transc.GAUGE_MIN"
"FTC1" > "HOL4Real.transc.FTC1"
"FINE_MIN" > "HOL4Real.transc.FINE_MIN"
"EXP_TOTAL_LEMMA" > "HOL4Real.transc.EXP_TOTAL_LEMMA"
"EXP_TOTAL" > "HOL4Real.transc.EXP_TOTAL"
"EXP_SUB" > "HOL4Real.transc.EXP_SUB"
"EXP_POS_LT" > "HOL4Real.transc.EXP_POS_LT"
"EXP_POS_LE" > "HOL4Real.transc.EXP_POS_LE"
"EXP_NZ" > "HOL4Real.transc.EXP_NZ"
"EXP_NEG_MUL2" > "HOL4Real.transc.EXP_NEG_MUL2"
"EXP_NEG_MUL" > "HOL4Real.transc.EXP_NEG_MUL"
"EXP_NEG" > "HOL4Real.transc.EXP_NEG"
"EXP_N" > "HOL4Real.transc.EXP_N"
"EXP_MONO_LT" > "HOL4Real.transc.EXP_MONO_LT"
"EXP_MONO_LE" > "HOL4Real.transc.EXP_MONO_LE"
"EXP_MONO_IMP" > "HOL4Real.transc.EXP_MONO_IMP"
"EXP_LT_1" > "HOL4Real.transc.EXP_LT_1"
"EXP_LN" > "HOL4Real.transc.EXP_LN"
"EXP_LE_X" > "HOL4Real.transc.EXP_LE_X"
"EXP_INJ" > "HOL4Real.transc.EXP_INJ"
"EXP_FDIFF" > "HOL4Real.transc.EXP_FDIFF"
"EXP_CONVERGES" > "HOL4Real.transc.EXP_CONVERGES"
"EXP_ADD_MUL" > "HOL4Real.transc.EXP_ADD_MUL"
"EXP_ADD" > "HOL4Real.transc.EXP_ADD"
"EXP_0" > "HOL4Real.transc.EXP_0"
"Dint_def" > "HOL4Real.transc.Dint_def"
"Dint" > "HOL4Real.transc.Dint"
"DIVISION_UBOUND_LT" > "HOL4Real.transc.DIVISION_UBOUND_LT"
"DIVISION_UBOUND" > "HOL4Real.transc.DIVISION_UBOUND"
"DIVISION_THM" > "HOL4Real.transc.DIVISION_THM"
"DIVISION_SINGLE" > "HOL4Real.transc.DIVISION_SINGLE"
"DIVISION_RHS" > "HOL4Real.transc.DIVISION_RHS"
"DIVISION_LT_GEN" > "HOL4Real.transc.DIVISION_LT_GEN"
"DIVISION_LT" > "HOL4Real.transc.DIVISION_LT"
"DIVISION_LHS" > "HOL4Real.transc.DIVISION_LHS"
"DIVISION_LE" > "HOL4Real.transc.DIVISION_LE"
"DIVISION_LBOUND_LT" > "HOL4Real.transc.DIVISION_LBOUND_LT"
"DIVISION_LBOUND" > "HOL4Real.transc.DIVISION_LBOUND"
"DIVISION_GT" > "HOL4Real.transc.DIVISION_GT"
"DIVISION_EXISTS" > "HOL4Real.transc.DIVISION_EXISTS"
"DIVISION_EQ" > "HOL4Real.transc.DIVISION_EQ"
"DIVISION_APPEND" > "HOL4Real.transc.DIVISION_APPEND"
"DIVISION_1" > "HOL4Real.transc.DIVISION_1"
"DIVISION_0" > "HOL4Real.transc.DIVISION_0"
"DINT_UNIQ" > "HOL4Real.transc.DINT_UNIQ"
"DIFF_TAN" > "HOL4Real.transc.DIFF_TAN"
"DIFF_SIN" > "HOL4Real.transc.DIFF_SIN"
"DIFF_LN_COMPOSITE" > "HOL4Real.transc.DIFF_LN_COMPOSITE"
"DIFF_LN" > "HOL4Real.transc.DIFF_LN"
"DIFF_EXP" > "HOL4Real.transc.DIFF_EXP"
"DIFF_COS" > "HOL4Real.transc.DIFF_COS"
"DIFF_COMPOSITE" > "HOL4Real.transc.DIFF_COMPOSITE"
"DIFF_ATN" > "HOL4Real.transc.DIFF_ATN"
"DIFF_ASN_LEMMA" > "HOL4Real.transc.DIFF_ASN_LEMMA"
"DIFF_ASN" > "HOL4Real.transc.DIFF_ASN"
"DIFF_ACS_LEMMA" > "HOL4Real.transc.DIFF_ACS_LEMMA"
"DIFF_ACS" > "HOL4Real.transc.DIFF_ACS"
"COS_ZERO_LEMMA" > "HOL4Real.transc.COS_ZERO_LEMMA"
"COS_ZERO" > "HOL4Real.transc.COS_ZERO"
"COS_TOTAL" > "HOL4Real.transc.COS_TOTAL"
"COS_SIN_SQRT" > "HOL4Real.transc.COS_SIN_SQRT"
"COS_SIN_SQ" > "HOL4Real.transc.COS_SIN_SQ"
"COS_SIN" > "HOL4Real.transc.COS_SIN"
"COS_POS_PI_LE" > "HOL4Real.transc.COS_POS_PI_LE"
"COS_POS_PI2_LE" > "HOL4Real.transc.COS_POS_PI2_LE"
"COS_POS_PI2" > "HOL4Real.transc.COS_POS_PI2"
"COS_POS_PI" > "HOL4Real.transc.COS_POS_PI"
"COS_PI2" > "HOL4Real.transc.COS_PI2"
"COS_PI" > "HOL4Real.transc.COS_PI"
"COS_PERIODIC_PI" > "HOL4Real.transc.COS_PERIODIC_PI"
"COS_PERIODIC" > "HOL4Real.transc.COS_PERIODIC"
"COS_PAIRED" > "HOL4Real.transc.COS_PAIRED"
"COS_NPI" > "HOL4Real.transc.COS_NPI"
"COS_NEG" > "HOL4Real.transc.COS_NEG"
"COS_ISZERO" > "HOL4Real.transc.COS_ISZERO"
"COS_FDIFF" > "HOL4Real.transc.COS_FDIFF"
"COS_DOUBLE" > "HOL4Real.transc.COS_DOUBLE"
"COS_CONVERGES" > "HOL4Real.transc.COS_CONVERGES"
"COS_BOUNDS" > "HOL4Real.transc.COS_BOUNDS"
"COS_BOUND" > "HOL4Real.transc.COS_BOUND"
"COS_ATN_NZ" > "HOL4Real.transc.COS_ATN_NZ"
"COS_ASN_NZ" > "HOL4Real.transc.COS_ASN_NZ"
"COS_ADD" > "HOL4Real.transc.COS_ADD"
"COS_ACS" > "HOL4Real.transc.COS_ACS"
"COS_2" > "HOL4Real.transc.COS_2"
"COS_0" > "HOL4Real.transc.COS_0"
"ATN_TAN" > "HOL4Real.transc.ATN_TAN"
"ATN_BOUNDS" > "HOL4Real.transc.ATN_BOUNDS"
"ATN" > "HOL4Real.transc.ATN"
"ASN_SIN" > "HOL4Real.transc.ASN_SIN"
"ASN_BOUNDS_LT" > "HOL4Real.transc.ASN_BOUNDS_LT"
"ASN_BOUNDS" > "HOL4Real.transc.ASN_BOUNDS"
"ASN" > "HOL4Real.transc.ASN"
"ACS_COS" > "HOL4Real.transc.ACS_COS"
"ACS_BOUNDS_LT" > "HOL4Real.transc.ACS_BOUNDS_LT"
"ACS_BOUNDS" > "HOL4Real.transc.ACS_BOUNDS"
"ACS" > "HOL4Real.transc.ACS"
end