renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
import
import_segment "hol4"
def_maps
"sup" > "sup_def"
"sumc" > "sumc_def"
"sum" > "sum_def"
const_maps
"sup" > "HOL4Real.real.sup"
"sum" > "HOL4Real.real.sum"
"real_sub" > "Groups.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
"real_lte" > "Orderings.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"pow" > "Power.power_class.power" :: "real => nat => real"
"abs" > "Groups.abs" :: "real => real"
"/" > "Ring.divide" :: "real => real => real"
thm_maps
"sup_def" > "HOL4Real.real.sup_def"
"sup" > "HOL4Real.real.sup"
"sumc" > "HOL4Real.real.sumc"
"sum_def" > "HOL4Real.real.sum_def"
"sum" > "HOL4Real.real.sum"
"real_sub" > "Groups.diff_def"
"real_of_num" > "HOL4Compat.real_of_num"
"real_lte" > "HOL4Compat.real_lte"
"real_lt" > "Orderings.linorder_not_le"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"real_div" > "Ring.divide_inverse"
"pow" > "HOL4Compat.pow"
"abs" > "HOL4Compat.abs"
"SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3"
"SUP_LEMMA2" > "HOL4Real.real.SUP_LEMMA2"
"SUP_LEMMA1" > "HOL4Real.real.SUP_LEMMA1"
"SUM_ZERO" > "HOL4Real.real.SUM_ZERO"
"SUM_TWO" > "HOL4Real.real.SUM_TWO"
"SUM_SUBST" > "HOL4Real.real.SUM_SUBST"
"SUM_SUB" > "HOL4Real.real.SUM_SUB"
"SUM_REINDEX" > "HOL4Real.real.SUM_REINDEX"
"SUM_POS_GEN" > "HOL4Real.real.SUM_POS_GEN"
"SUM_POS" > "HOL4Real.real.SUM_POS"
"SUM_PERMUTE_0" > "HOL4Real.real.SUM_PERMUTE_0"
"SUM_OFFSET" > "HOL4Real.real.SUM_OFFSET"
"SUM_NSUB" > "HOL4Real.real.SUM_NSUB"
"SUM_NEG" > "HOL4Real.real.SUM_NEG"
"SUM_LE" > "HOL4Real.real.SUM_LE"
"SUM_GROUP" > "HOL4Real.real.SUM_GROUP"
"SUM_EQ" > "HOL4Real.real.SUM_EQ"
"SUM_DIFF" > "HOL4Real.real.SUM_DIFF"
"SUM_DEF" > "HOL4Real.real.SUM_DEF"
"SUM_CMUL" > "HOL4Real.real.SUM_CMUL"
"SUM_CANCEL" > "HOL4Real.real.SUM_CANCEL"
"SUM_BOUND" > "HOL4Real.real.SUM_BOUND"
"SUM_ADD" > "HOL4Real.real.SUM_ADD"
"SUM_ABS_LE" > "HOL4Real.real.SUM_ABS_LE"
"SUM_ABS" > "HOL4Real.real.SUM_ABS"
"SUM_2" > "HOL4Real.real.SUM_2"
"SUM_1" > "HOL4Real.real.SUM_1"
"SUM_0" > "HOL4Real.real.SUM_0"
"SETOK_LE_LT" > "HOL4Real.real.SETOK_LE_LT"
"REAL_SUP_UBOUND_LE" > "HOL4Real.real.REAL_SUP_UBOUND_LE"
"REAL_SUP_UBOUND" > "HOL4Real.real.REAL_SUP_UBOUND"
"REAL_SUP_SOMEPOS" > "HOL4Real.real.REAL_SUP_SOMEPOS"
"REAL_SUP_LE" > "HOL4Real.real.REAL_SUP_LE"
"REAL_SUP_EXISTS" > "HOL4Real.real.REAL_SUP_EXISTS"
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
"REAL_SUP" > "HOL4Real.real.REAL_SUP"
"REAL_SUMSQ" > "HOL4Real.real.REAL_SUMSQ"
"REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE"
"REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2"
"REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB"
"REAL_SUB_RZERO" > "Groups.diff_0_right"
"REAL_SUB_RNEG" > "Groups.diff_minus_eq_add"
"REAL_SUB_REFL" > "Groups.diff_self"
"REAL_SUB_RDISTRIB" > "Rings.ring_eq_simps_3"
"REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
"REAL_SUB_LZERO" > "Groups.diff_0"
"REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT"
"REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
"REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE"
"REAL_SUB_LDISTRIB" > "Rings.ring_eq_simps_4"
"REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
"REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2"
"REAL_SUB_ADD" > "Groups.diff_add_cancel"
"REAL_SUB_ABS" > "Groups.abs_triangle_ineq2"
"REAL_SUB_0" > "Groups.diff_eq_0_iff_eq"
"REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
"REAL_RINV_UNIQ" > "Rings.inverse_unique"
"REAL_RDISTRIB" > "Rings.ring_eq_simps_1"
"REAL_POW_POW" > "Power.power_mult"
"REAL_POW_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT"
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
"REAL_POW_LT" > "Power.zero_less_power"
"REAL_POW_INV" > "Power.power_inverse"
"REAL_POW_DIV" > "Power.power_divide"
"REAL_POW_ADD" > "Power.power_add"
"REAL_POW2_ABS" > "Nat_Numeral.power2_abs"
"REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ"
"REAL_POS" > "RealDef.real_of_nat_ge_zero"
"REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
"REAL_OVER1" > "Rings.divide_1"
"REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc"
"REAL_OF_NUM_POW" > "RealDef.power_real_of_nat"
"REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult"
"REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff"
"REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject"
"REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add"
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
"REAL_NOT_LT" > "HOL4Compat.real_lte"
"REAL_NOT_LE" > "Orderings.linorder_not_le"
"REAL_NEG_SUB" > "Groups.minus_diff_eq"
"REAL_NEG_RMUL" > "Rings.mult_minus_right"
"REAL_NEG_NEG" > "Groups.minus_minus"
"REAL_NEG_MUL2" > "Rings.minus_mult_minus"
"REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1"
"REAL_NEG_LT0" > "Groups.neg_less_0_iff_less"
"REAL_NEG_LMUL" > "Rings.mult_minus_left"
"REAL_NEG_LE0" > "Groups.neg_le_0_iff_le"
"REAL_NEG_INV" > "Rings.nonzero_inverse_minus_eq"
"REAL_NEG_GT0" > "Groups.neg_0_less_iff_less"
"REAL_NEG_GE0" > "Groups.neg_0_le_iff_le"
"REAL_NEG_EQ0" > "Groups.neg_equal_0_iff_equal"
"REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ"
"REAL_NEG_ADD" > "Groups.minus_add_distrib"
"REAL_NEG_0" > "Groups.minus_zero"
"REAL_NEGNEG" > "Groups.minus_minus"
"REAL_MUL_SYM" > "Int.zmult_ac_2"
"REAL_MUL_RZERO" > "Rings.mult_zero_right"
"REAL_MUL_RNEG" > "Rings.mult_minus_right"
"REAL_MUL_RINV" > "Rings.right_inverse"
"REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident"
"REAL_MUL_LZERO" > "Rings.mult_zero_left"
"REAL_MUL_LNEG" > "Rings.mult_minus_left"
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
"REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
"REAL_MUL" > "RealDef.real_of_nat_mult"
"REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2"
"REAL_MIDDLE1" > "HOL4Real.real.REAL_MIDDLE1"
"REAL_MEAN" > "Rings.dense"
"REAL_LT_TRANS" > "Set.basic_trans_rules_21"
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
"REAL_LT_SUB_RADD" > "Groups.compare_rls_6"
"REAL_LT_SUB_LADD" > "Groups.compare_rls_7"
"REAL_LT_RMUL_IMP" > "Rings.mult_strict_right_mono"
"REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0"
"REAL_LT_RMUL" > "RealDef.real_mult_less_iff1"
"REAL_LT_REFL" > "Orderings.order_less_irrefl"
"REAL_LT_RDIV_EQ" > "Rings.pos_less_divide_eq"
"REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0"
"REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV"
"REAL_LT_RADD" > "Groups.add_less_cancel_right"
"REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ"
"REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL"
"REAL_LT_NEG" > "Groups.neg_less_iff_less"
"REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
"REAL_LT_MUL2" > "Rings.mult_strict_mono'"
"REAL_LT_MUL" > "Rings.mult_pos_pos"
"REAL_LT_LMUL_IMP" > "Rings.linordered_comm_semiring_strict_class.mult_strict_mono"
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
"REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
"REAL_LT_LE" > "Orderings.order_class.order_less_le"
"REAL_LT_LDIV_EQ" > "Rings.pos_divide_less_eq"
"REAL_LT_LADD" > "Groups.add_less_cancel_left"
"REAL_LT_INV_EQ" > "Rings.inverse_positive_iff_positive"
"REAL_LT_INV" > "Rings.less_imp_inverse_less"
"REAL_LT_IMP_NE" > "Orderings.less_imp_neq"
"REAL_LT_IMP_LE" > "Orderings.order_less_imp_le"
"REAL_LT_IADD" > "Groups.add_strict_left_mono"
"REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2"
"REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff"
"REAL_LT_GT" > "Orderings.order_less_not_sym"
"REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0"
"REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION"
"REAL_LT_DIV" > "Rings.divide_pos_pos"
"REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM"
"REAL_LT_ADD_SUB" > "Groups.compare_rls_7"
"REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR"
"REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2"
"REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG"
"REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
"REAL_LT_ADD2" > "Groups.add_strict_mono"
"REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
"REAL_LT_ADD" > "Groups.add_pos_pos"
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
"REAL_LT_01" > "Rings.zero_less_one"
"REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
"REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
"REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
"REAL_LTE_ADD2" > "Groups.add_less_le_mono"
"REAL_LTE_ADD" > "Groups.add_pos_nonneg"
"REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2"
"REAL_LT" > "RealDef.real_of_nat_less_iff"
"REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ"
"REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ"
"REAL_LE_TRANS" > "Set.basic_trans_rules_25"
"REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear"
"REAL_LE_SUB_RADD" > "Groups.compare_rls_8"
"REAL_LE_SUB_LADD" > "Groups.compare_rls_9"
"REAL_LE_SQUARE" > "Rings.zero_le_square"
"REAL_LE_RNEG" > "Groups.le_eq_neg"
"REAL_LE_RMUL_IMP" > "Rings.mult_right_mono"
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
"REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl"
"REAL_LE_RDIV_EQ" > "Rings.pos_le_divide_eq"
"REAL_LE_RDIV" > "Rings.mult_imp_le_div_pos"
"REAL_LE_RADD" > "Groups.add_le_cancel_right"
"REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12"
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
"REAL_LE_NEGR" > "Groups.le_minus_self_iff"
"REAL_LE_NEGL" > "Groups.minus_le_self_iff"
"REAL_LE_NEG2" > "Groups.neg_le_iff_le"
"REAL_LE_NEG" > "Groups.neg_le_iff_le"
"REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
"REAL_LE_MUL" > "Rings.mult_nonneg_nonneg"
"REAL_LE_LT" > "Orderings.order_le_less"
"REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
"REAL_LE_LMUL_IMP" > "Rings.mult_mono"
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
"REAL_LE_LDIV_EQ" > "Rings.pos_divide_le_eq"
"REAL_LE_LDIV" > "Rings.mult_imp_div_pos_le"
"REAL_LE_LADD_IMP" > "Groups.add_left_mono"
"REAL_LE_LADD" > "Groups.add_le_cancel_left"
"REAL_LE_INV_EQ" > "Rings.inverse_nonnegative_iff_nonnegative"
"REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV"
"REAL_LE_DOUBLE" > "Groups.zero_le_double_add_iff_zero_le_single_add"
"REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"
"REAL_LE_ANTISYM" > "Orderings.order_eq_iff"
"REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR"
"REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL"
"REAL_LE_ADD2" > "Groups.add_mono"
"REAL_LE_ADD" > "Groups.add_nonneg_nonneg"
"REAL_LE_01" > "Rings.zero_le_one"
"REAL_LET_TRANS" > "Set.basic_trans_rules_23"
"REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear"
"REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM"
"REAL_LET_ADD2" > "Groups.add_le_less_mono"
"REAL_LET_ADD" > "Groups.add_nonneg_pos"
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
"REAL_LE" > "RealDef.real_of_nat_le_iff"
"REAL_LDISTRIB" > "Rings.ring_eq_simps_2"
"REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
"REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
"REAL_INV_LT1" > "Fields.one_less_inverse"
"REAL_INV_INV" > "Rings.inverse_inverse_eq"
"REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
"REAL_INV_1OVER" > "Rings.inverse_eq_divide"
"REAL_INV_0" > "Rings.division_ring_inverse_zero_class.inverse_zero"
"REAL_INVINV" > "Rings.nonzero_inverse_inverse_eq"
"REAL_INV1" > "Rings.inverse_1"
"REAL_INJ" > "RealDef.real_of_nat_inject"
"REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
"REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"
"REAL_EQ_SUB_RADD" > "Rings.ring_eq_simps_15"
"REAL_EQ_SUB_LADD" > "Rings.ring_eq_simps_16"
"REAL_EQ_RMUL_IMP" > "Rings.field_mult_cancel_right_lemma"
"REAL_EQ_RMUL" > "Rings.field_mult_cancel_right"
"REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ"
"REAL_EQ_RADD" > "Groups.add_right_cancel"
"REAL_EQ_NEG" > "Groups.neg_equal_iff_equal"
"REAL_EQ_MUL_LCANCEL" > "Rings.field_mult_cancel_left"
"REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP"
"REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel"
"REAL_EQ_LMUL" > "Rings.field_mult_cancel_left"
"REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ"
"REAL_EQ_LADD" > "Groups.add_left_cancel"
"REAL_EQ_IMP_LE" > "Orderings.order_eq_refl"
"REAL_ENTIRE" > "Rings.field_mult_eq_0_iff"
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN"
"REAL_DOUBLE" > "Int.mult_2"
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
"REAL_DIV_REFL" > "Rings.divide_self"
"REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
"REAL_DIV_LZERO" > "Rings.divide_zero_left"
"REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL"
"REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
"REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
"REAL_ARCH" > "RComplete.reals_Archimedean3"
"REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
"REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
"REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB"
"REAL_ADD_RINV" > "Groups.right_minus"
"REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
"REAL_ADD_RID" > "Finite_Set.AC_add.f_e.ident"
"REAL_ADD_RDISTRIB" > "Rings.ring_eq_simps_1"
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
"REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
"REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
"REAL_ADD_LDISTRIB" > "Rings.ring_eq_simps_2"
"REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
"REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
"REAL_ADD" > "RealDef.real_of_nat_add"
"REAL_ABS_TRIANGLE" > "Groups.abs_triangle_ineq"
"REAL_ABS_POS" > "Groups.abs_ge_zero"
"REAL_ABS_MUL" > "Rings.abs_mult"
"REAL_ABS_0" > "Int.bin_arith_simps_28"
"REAL_10" > "HOL4Compat.REAL_10"
"REAL_1" > "HOL4Real.real.REAL_1"
"REAL_0" > "HOL4Real.real.REAL_0"
"REAL" > "RealDef.real_of_nat_Suc"
"POW_ZERO_EQ" > "HOL4Real.real.POW_ZERO_EQ"
"POW_ZERO" > "RealPow.realpow_zero_zero"
"POW_POS_LT" > "HOL4Real.real.POW_POS_LT"
"POW_POS" > "Power.zero_le_power"
"POW_PLUS1" > "HOL4Real.real.POW_PLUS1"
"POW_ONE" > "Power.power_one"
"POW_NZ" > "Power.field_power_not_zero"
"POW_MUL" > "Power.power_mult_distrib"
"POW_MINUS1" > "Nat_Numeral.power_minus1_even"
"POW_M1" > "HOL4Real.real.POW_M1"
"POW_LT" > "HOL4Real.real.POW_LT"
"POW_LE" > "Power.power_mono"
"POW_INV" > "Power.nonzero_power_inverse"
"POW_EQ" > "Power.power_inject_base"
"POW_ADD" > "Power.power_add"
"POW_ABS" > "Power.power_abs"
"POW_2_LT" > "RealPow.two_realpow_gt"
"POW_2_LE1" > "RealPow.two_realpow_ge_one"
"POW_2" > "Nat_Numeral.power2_eq_square"
"POW_1" > "Power.power_one_right"
"POW_0" > "Power.power_0_Suc"
"ABS_ZERO" > "Groups.abs_eq_0"
"ABS_TRIANGLE" > "Groups.abs_triangle_ineq"
"ABS_SUM" > "HOL4Real.real.ABS_SUM"
"ABS_SUB_ABS" > "Groups.abs_triangle_ineq3"
"ABS_SUB" > "Groups.abs_minus_commute"
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ"
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
"ABS_REFL" > "HOL4Real.real.ABS_REFL"
"ABS_POW2" > "Nat_Numeral.abs_power2"
"ABS_POS" > "Groups.abs_ge_zero"
"ABS_NZ" > "Groups.zero_less_abs_iff"
"ABS_NEG" > "Groups.abs_minus_cancel"
"ABS_N" > "RealDef.abs_real_of_nat_cancel"
"ABS_MUL" > "Rings.abs_mult"
"ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2"
"ABS_LE" > "Groups.abs_ge_self"
"ABS_INV" > "Rings.nonzero_abs_inverse"
"ABS_DIV" > "Rings.nonzero_abs_divide"
"ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE"
"ABS_CASES" > "HOL4Real.real.ABS_CASES"
"ABS_BOUNDS" > "RealDef.abs_le_interval_iff"
"ABS_BOUND" > "HOL4Real.real.ABS_BOUND"
"ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2"
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
"ABS_ABS" > "Groups.abs_idempotent"
"ABS_1" > "Int.bin_arith_simps_29"
"ABS_0" > "Int.bin_arith_simps_28"
end