import
import_segment "hol4"
def_maps
"isacut" > "isacut_def"
"hreal_sup" > "hreal_sup_def"
"hreal_sub" > "hreal_sub_def"
"hreal_mul" > "hreal_mul_def"
"hreal_lt" > "hreal_lt_def"
"hreal_inv" > "hreal_inv_def"
"hreal_add" > "hreal_add_def"
"hreal_1" > "hreal_1_def"
"hreal" > "hreal_def"
"hrat_lt" > "hrat_lt_def"
"cut_of_hrat" > "cut_of_hrat_def"
"cut" > "cut_def"
type_maps
"hreal" > "HOL4Base.hreal.hreal"
const_maps
"isacut" > "HOL4Base.hreal.isacut"
"hreal_sup" > "HOL4Base.hreal.hreal_sup"
"hreal_sub" > "HOL4Base.hreal.hreal_sub"
"hreal_mul" > "HOL4Base.hreal.hreal_mul"
"hreal_lt" > "HOL4Base.hreal.hreal_lt"
"hreal_inv" > "HOL4Base.hreal.hreal_inv"
"hreal_add" > "HOL4Base.hreal.hreal_add"
"hreal_1" > "HOL4Base.hreal.hreal_1"
"hrat_lt" > "HOL4Base.hreal.hrat_lt"
"cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
thm_maps
"isacut_def" > "HOL4Base.hreal.isacut_def"
"isacut" > "HOL4Base.hreal.isacut"
"hreal_tybij" > "HOL4Base.hreal.hreal_tybij"
"hreal_sup_def" > "HOL4Base.hreal.hreal_sup_def"
"hreal_sup" > "HOL4Base.hreal.hreal_sup"
"hreal_sub_def" > "HOL4Base.hreal.hreal_sub_def"
"hreal_sub" > "HOL4Base.hreal.hreal_sub"
"hreal_mul_def" > "HOL4Base.hreal.hreal_mul_def"
"hreal_mul" > "HOL4Base.hreal.hreal_mul"
"hreal_lt_def" > "HOL4Base.hreal.hreal_lt_def"
"hreal_lt" > "HOL4Base.hreal.hreal_lt"
"hreal_inv_def" > "HOL4Base.hreal.hreal_inv_def"
"hreal_inv" > "HOL4Base.hreal.hreal_inv"
"hreal_add_def" > "HOL4Base.hreal.hreal_add_def"
"hreal_add" > "HOL4Base.hreal.hreal_add"
"hreal_TY_DEF" > "HOL4Base.hreal.hreal_TY_DEF"
"hreal_1_def" > "HOL4Base.hreal.hreal_1_def"
"hreal_1" > "HOL4Base.hreal.hreal_1"
"hrat_lt_def" > "HOL4Base.hreal.hrat_lt_def"
"hrat_lt" > "HOL4Base.hreal.hrat_lt"
"cut_of_hrat_def" > "HOL4Base.hreal.cut_of_hrat_def"
"cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
"ISACUT_HRAT" > "HOL4Base.hreal.ISACUT_HRAT"
"HREAL_SUP_ISACUT" > "HOL4Base.hreal.HREAL_SUP_ISACUT"
"HREAL_SUP" > "HOL4Base.hreal.HREAL_SUP"
"HREAL_SUB_ISACUT" > "HOL4Base.hreal.HREAL_SUB_ISACUT"
"HREAL_SUB_ADD" > "HOL4Base.hreal.HREAL_SUB_ADD"
"HREAL_NOZERO" > "HOL4Base.hreal.HREAL_NOZERO"
"HREAL_MUL_SYM" > "HOL4Base.hreal.HREAL_MUL_SYM"
"HREAL_MUL_LINV" > "HOL4Base.hreal.HREAL_MUL_LINV"
"HREAL_MUL_LID" > "HOL4Base.hreal.HREAL_MUL_LID"
"HREAL_MUL_ISACUT" > "HOL4Base.hreal.HREAL_MUL_ISACUT"
"HREAL_MUL_ASSOC" > "HOL4Base.hreal.HREAL_MUL_ASSOC"
"HREAL_LT_TOTAL" > "HOL4Base.hreal.HREAL_LT_TOTAL"
"HREAL_LT_LEMMA" > "HOL4Base.hreal.HREAL_LT_LEMMA"
"HREAL_LT" > "HOL4Base.hreal.HREAL_LT"
"HREAL_LDISTRIB" > "HOL4Base.hreal.HREAL_LDISTRIB"
"HREAL_INV_ISACUT" > "HOL4Base.hreal.HREAL_INV_ISACUT"
"HREAL_ADD_TOTAL" > "HOL4Base.hreal.HREAL_ADD_TOTAL"
"HREAL_ADD_SYM" > "HOL4Base.hreal.HREAL_ADD_SYM"
"HREAL_ADD_ISACUT" > "HOL4Base.hreal.HREAL_ADD_ISACUT"
"HREAL_ADD_ASSOC" > "HOL4Base.hreal.HREAL_ADD_ASSOC"
"HRAT_UP" > "HOL4Base.hreal.HRAT_UP"
"HRAT_RDISTRIB" > "HOL4Base.hreal.HRAT_RDISTRIB"
"HRAT_MUL_RINV" > "HOL4Base.hreal.HRAT_MUL_RINV"
"HRAT_MUL_RID" > "HOL4Base.hreal.HRAT_MUL_RID"
"HRAT_MEAN" > "HOL4Base.hreal.HRAT_MEAN"
"HRAT_LT_TRANS" > "HOL4Base.hreal.HRAT_LT_TRANS"
"HRAT_LT_TOTAL" > "HOL4Base.hreal.HRAT_LT_TOTAL"
"HRAT_LT_RMUL1" > "HOL4Base.hreal.HRAT_LT_RMUL1"
"HRAT_LT_RMUL" > "HOL4Base.hreal.HRAT_LT_RMUL"
"HRAT_LT_REFL" > "HOL4Base.hreal.HRAT_LT_REFL"
"HRAT_LT_RADD" > "HOL4Base.hreal.HRAT_LT_RADD"
"HRAT_LT_R1" > "HOL4Base.hreal.HRAT_LT_R1"
"HRAT_LT_NE" > "HOL4Base.hreal.HRAT_LT_NE"
"HRAT_LT_MUL2" > "HOL4Base.hreal.HRAT_LT_MUL2"
"HRAT_LT_LMUL1" > "HOL4Base.hreal.HRAT_LT_LMUL1"
"HRAT_LT_LMUL" > "HOL4Base.hreal.HRAT_LT_LMUL"
"HRAT_LT_LADD" > "HOL4Base.hreal.HRAT_LT_LADD"
"HRAT_LT_L1" > "HOL4Base.hreal.HRAT_LT_L1"
"HRAT_LT_GT" > "HOL4Base.hreal.HRAT_LT_GT"
"HRAT_LT_ANTISYM" > "HOL4Base.hreal.HRAT_LT_ANTISYM"
"HRAT_LT_ADDR" > "HOL4Base.hreal.HRAT_LT_ADDR"
"HRAT_LT_ADDL" > "HOL4Base.hreal.HRAT_LT_ADDL"
"HRAT_LT_ADD2" > "HOL4Base.hreal.HRAT_LT_ADD2"
"HRAT_INV_MUL" > "HOL4Base.hreal.HRAT_INV_MUL"
"HRAT_GT_LMUL1" > "HOL4Base.hreal.HRAT_GT_LMUL1"
"HRAT_GT_L1" > "HOL4Base.hreal.HRAT_GT_L1"
"HRAT_EQ_LMUL" > "HOL4Base.hreal.HRAT_EQ_LMUL"
"HRAT_EQ_LADD" > "HOL4Base.hreal.HRAT_EQ_LADD"
"HRAT_DOWN2" > "HOL4Base.hreal.HRAT_DOWN2"
"HRAT_DOWN" > "HOL4Base.hreal.HRAT_DOWN"
"EQUAL_CUTS" > "HOL4Base.hreal.EQUAL_CUTS"
"CUT_UP" > "HOL4Base.hreal.CUT_UP"
"CUT_UBOUND" > "HOL4Base.hreal.CUT_UBOUND"
"CUT_STRADDLE" > "HOL4Base.hreal.CUT_STRADDLE"
"CUT_NONEMPTY" > "HOL4Base.hreal.CUT_NONEMPTY"
"CUT_NEARTOP_MUL" > "HOL4Base.hreal.CUT_NEARTOP_MUL"
"CUT_NEARTOP_ADD" > "HOL4Base.hreal.CUT_NEARTOP_ADD"
"CUT_ISACUT" > "HOL4Base.hreal.CUT_ISACUT"
"CUT_DOWN" > "HOL4Base.hreal.CUT_DOWN"
"CUT_BOUNDED" > "HOL4Base.hreal.CUT_BOUNDED"
end