src/HOL/Import/HOL/real.imp
author haftmann
Mon Feb 08 17:12:38 2010 +0100 (2010-02-08)
changeset 35050 9f841f20dca6
parent 35028 108662d50512
child 35085 22bdb7f86a1e
permissions -rw-r--r--
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "sup" > "sup_def"
     7   "sumc" > "sumc_def"
     8   "sum" > "sum_def"
     9 
    10 const_maps
    11   "sup" > "HOL4Real.real.sup"
    12   "sum" > "HOL4Real.real.sum"
    13   "real_sub" > "Algebras.minus" :: "real => real => real"
    14   "real_of_num" > "RealDef.real" :: "nat => real"
    15   "real_lte" > "Algebras.less_eq" :: "real => real => bool"
    16   "real_gt" > "HOL4Compat.real_gt"
    17   "real_ge" > "HOL4Compat.real_ge"
    18   "pow" > "Power.power_class.power" :: "real => nat => real"
    19   "abs" > "Algebras.abs" :: "real => real"
    20   "/" > "Algebras.divide" :: "real => real => real"
    21 
    22 thm_maps
    23   "sup_def" > "HOL4Real.real.sup_def"
    24   "sup" > "HOL4Real.real.sup"
    25   "sumc" > "HOL4Real.real.sumc"
    26   "sum_def" > "HOL4Real.real.sum_def"
    27   "sum" > "HOL4Real.real.sum"
    28   "real_sub" > "Groups.diff_def"
    29   "real_of_num" > "HOL4Compat.real_of_num"
    30   "real_lte" > "HOL4Compat.real_lte"
    31   "real_lt" > "Orderings.linorder_not_le"
    32   "real_gt" > "HOL4Compat.real_gt"
    33   "real_ge" > "HOL4Compat.real_ge"
    34   "real_div" > "Rings.field_class.divide_inverse"
    35   "pow" > "HOL4Compat.pow"
    36   "abs" > "HOL4Compat.abs"
    37   "SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3"
    38   "SUP_LEMMA2" > "HOL4Real.real.SUP_LEMMA2"
    39   "SUP_LEMMA1" > "HOL4Real.real.SUP_LEMMA1"
    40   "SUM_ZERO" > "HOL4Real.real.SUM_ZERO"
    41   "SUM_TWO" > "HOL4Real.real.SUM_TWO"
    42   "SUM_SUBST" > "HOL4Real.real.SUM_SUBST"
    43   "SUM_SUB" > "HOL4Real.real.SUM_SUB"
    44   "SUM_REINDEX" > "HOL4Real.real.SUM_REINDEX"
    45   "SUM_POS_GEN" > "HOL4Real.real.SUM_POS_GEN"
    46   "SUM_POS" > "HOL4Real.real.SUM_POS"
    47   "SUM_PERMUTE_0" > "HOL4Real.real.SUM_PERMUTE_0"
    48   "SUM_OFFSET" > "HOL4Real.real.SUM_OFFSET"
    49   "SUM_NSUB" > "HOL4Real.real.SUM_NSUB"
    50   "SUM_NEG" > "HOL4Real.real.SUM_NEG"
    51   "SUM_LE" > "HOL4Real.real.SUM_LE"
    52   "SUM_GROUP" > "HOL4Real.real.SUM_GROUP"
    53   "SUM_EQ" > "HOL4Real.real.SUM_EQ"
    54   "SUM_DIFF" > "HOL4Real.real.SUM_DIFF"
    55   "SUM_DEF" > "HOL4Real.real.SUM_DEF"
    56   "SUM_CMUL" > "HOL4Real.real.SUM_CMUL"
    57   "SUM_CANCEL" > "HOL4Real.real.SUM_CANCEL"
    58   "SUM_BOUND" > "HOL4Real.real.SUM_BOUND"
    59   "SUM_ADD" > "HOL4Real.real.SUM_ADD"
    60   "SUM_ABS_LE" > "HOL4Real.real.SUM_ABS_LE"
    61   "SUM_ABS" > "HOL4Real.real.SUM_ABS"
    62   "SUM_2" > "HOL4Real.real.SUM_2"
    63   "SUM_1" > "HOL4Real.real.SUM_1"
    64   "SUM_0" > "HOL4Real.real.SUM_0"
    65   "SETOK_LE_LT" > "HOL4Real.real.SETOK_LE_LT"
    66   "REAL_SUP_UBOUND_LE" > "HOL4Real.real.REAL_SUP_UBOUND_LE"
    67   "REAL_SUP_UBOUND" > "HOL4Real.real.REAL_SUP_UBOUND"
    68   "REAL_SUP_SOMEPOS" > "HOL4Real.real.REAL_SUP_SOMEPOS"
    69   "REAL_SUP_LE" > "HOL4Real.real.REAL_SUP_LE"
    70   "REAL_SUP_EXISTS" > "HOL4Real.real.REAL_SUP_EXISTS"
    71   "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
    72   "REAL_SUP" > "HOL4Real.real.REAL_SUP"
    73   "REAL_SUMSQ" > "HOL4Real.real.REAL_SUMSQ"
    74   "REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE"
    75   "REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2"
    76   "REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB"
    77   "REAL_SUB_RZERO" > "Groups.diff_0_right"
    78   "REAL_SUB_RNEG" > "Groups.diff_minus_eq_add"
    79   "REAL_SUB_REFL" > "Groups.diff_self"
    80   "REAL_SUB_RDISTRIB" > "Rings.ring_eq_simps_3"
    81   "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
    82   "REAL_SUB_LZERO" > "Groups.diff_0"
    83   "REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT"
    84   "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
    85   "REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE"
    86   "REAL_SUB_LDISTRIB" > "Rings.ring_eq_simps_4"
    87   "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
    88   "REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2"
    89   "REAL_SUB_ADD" > "Groups.diff_add_cancel"
    90   "REAL_SUB_ABS" > "Groups.abs_triangle_ineq2"
    91   "REAL_SUB_0" > "Groups.diff_eq_0_iff_eq"
    92   "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
    93   "REAL_RINV_UNIQ" > "Rings.inverse_unique"
    94   "REAL_RDISTRIB" > "Rings.ring_eq_simps_1"
    95   "REAL_POW_POW" > "Power.power_mult"
    96   "REAL_POW_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT"
    97   "REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
    98   "REAL_POW_LT" > "Power.zero_less_power"
    99   "REAL_POW_INV" > "Power.power_inverse"
   100   "REAL_POW_DIV" > "Power.power_divide"
   101   "REAL_POW_ADD" > "Power.power_add"
   102   "REAL_POW2_ABS" > "Nat_Numeral.power2_abs"
   103   "REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ"
   104   "REAL_POS" > "RealDef.real_of_nat_ge_zero"
   105   "REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
   106   "REAL_OVER1" > "Rings.divide_1"
   107   "REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc"
   108   "REAL_OF_NUM_POW" > "RealPow.realpow_real_of_nat"
   109   "REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult"
   110   "REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff"
   111   "REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject"
   112   "REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add"
   113   "REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
   114   "REAL_NOT_LT" > "HOL4Compat.real_lte"
   115   "REAL_NOT_LE" > "Orderings.linorder_not_le"
   116   "REAL_NEG_SUB" > "Groups.minus_diff_eq"
   117   "REAL_NEG_RMUL" > "Rings.mult_minus_right"
   118   "REAL_NEG_NEG" > "Groups.minus_minus"
   119   "REAL_NEG_MUL2" > "Rings.minus_mult_minus"
   120   "REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1"
   121   "REAL_NEG_LT0" > "Groups.neg_less_0_iff_less"
   122   "REAL_NEG_LMUL" > "Rings.mult_minus_left"
   123   "REAL_NEG_LE0" > "Groups.neg_le_0_iff_le"
   124   "REAL_NEG_INV" > "Rings.nonzero_inverse_minus_eq"
   125   "REAL_NEG_GT0" > "Groups.neg_0_less_iff_less"
   126   "REAL_NEG_GE0" > "Groups.neg_0_le_iff_le"
   127   "REAL_NEG_EQ0" > "Groups.neg_equal_0_iff_equal"
   128   "REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ"
   129   "REAL_NEG_ADD" > "Groups.minus_add_distrib"
   130   "REAL_NEG_0" > "Groups.minus_zero"
   131   "REAL_NEGNEG" > "Groups.minus_minus"
   132   "REAL_MUL_SYM" > "Int.zmult_ac_2"
   133   "REAL_MUL_RZERO" > "Rings.mult_zero_right"
   134   "REAL_MUL_RNEG" > "Rings.mult_minus_right"
   135   "REAL_MUL_RINV" > "Rings.right_inverse"
   136   "REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident"
   137   "REAL_MUL_LZERO" > "Rings.mult_zero_left"
   138   "REAL_MUL_LNEG" > "Rings.mult_minus_left"
   139   "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
   140   "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
   141   "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
   142   "REAL_MUL" > "RealDef.real_of_nat_mult"
   143   "REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2"
   144   "REAL_MIDDLE1" > "HOL4Real.real.REAL_MIDDLE1"
   145   "REAL_MEAN" > "Rings.dense"
   146   "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
   147   "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
   148   "REAL_LT_SUB_RADD" > "Groups.compare_rls_6"
   149   "REAL_LT_SUB_LADD" > "Groups.compare_rls_7"
   150   "REAL_LT_RMUL_IMP" > "Rings.mult_strict_right_mono"
   151   "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0"
   152   "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1"
   153   "REAL_LT_REFL" > "Orderings.order_less_irrefl"
   154   "REAL_LT_RDIV_EQ" > "Rings.pos_less_divide_eq"
   155   "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0"
   156   "REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV"
   157   "REAL_LT_RADD" > "Groups.add_less_cancel_right"
   158   "REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ"
   159   "REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL"
   160   "REAL_LT_NEG" > "Groups.neg_less_iff_less"
   161   "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
   162   "REAL_LT_MUL2" > "Rings.mult_strict_mono'"
   163   "REAL_LT_MUL" > "Rings.mult_pos_pos"
   164   "REAL_LT_LMUL_IMP" > "Rings.linordered_comm_semiring_strict_class.mult_strict_mono"
   165   "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
   166   "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
   167   "REAL_LT_LE" > "Orderings.order_class.order_less_le"
   168   "REAL_LT_LDIV_EQ" > "Rings.pos_divide_less_eq"
   169   "REAL_LT_LADD" > "Groups.add_less_cancel_left"
   170   "REAL_LT_INV_EQ" > "Rings.inverse_positive_iff_positive"
   171   "REAL_LT_INV" > "Rings.less_imp_inverse_less"
   172   "REAL_LT_IMP_NE" > "Orderings.less_imp_neq"
   173   "REAL_LT_IMP_LE" > "Orderings.order_less_imp_le"
   174   "REAL_LT_IADD" > "Groups.add_strict_left_mono"
   175   "REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2"
   176   "REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff"
   177   "REAL_LT_GT" > "Orderings.order_less_not_sym"
   178   "REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0"
   179   "REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION"
   180   "REAL_LT_DIV" > "Rings.divide_pos_pos"
   181   "REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM"
   182   "REAL_LT_ADD_SUB" > "Groups.compare_rls_7"
   183   "REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR"
   184   "REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2"
   185   "REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG"
   186   "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
   187   "REAL_LT_ADD2" > "Groups.add_strict_mono"
   188   "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
   189   "REAL_LT_ADD" > "Groups.add_pos_pos"
   190   "REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
   191   "REAL_LT_01" > "Rings.zero_less_one"
   192   "REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
   193   "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
   194   "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
   195   "REAL_LTE_ADD2" > "Groups.add_less_le_mono"
   196   "REAL_LTE_ADD" > "Groups.add_pos_nonneg"
   197   "REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2"
   198   "REAL_LT" > "RealDef.real_of_nat_less_iff"
   199   "REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ"
   200   "REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ"
   201   "REAL_LE_TRANS" > "Set.basic_trans_rules_25"
   202   "REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear"
   203   "REAL_LE_SUB_RADD" > "Groups.compare_rls_8"
   204   "REAL_LE_SUB_LADD" > "Groups.compare_rls_9"
   205   "REAL_LE_SQUARE" > "Rings.zero_le_square"
   206   "REAL_LE_RNEG" > "Groups.le_eq_neg"
   207   "REAL_LE_RMUL_IMP" > "Rings.mult_right_mono"
   208   "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
   209   "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl"
   210   "REAL_LE_RDIV_EQ" > "Rings.pos_le_divide_eq"
   211   "REAL_LE_RDIV" > "Rings.mult_imp_le_div_pos"
   212   "REAL_LE_RADD" > "Groups.add_le_cancel_right"
   213   "REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12"
   214   "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
   215   "REAL_LE_NEGR" > "Groups.le_minus_self_iff"
   216   "REAL_LE_NEGL" > "Groups.minus_le_self_iff"
   217   "REAL_LE_NEG2" > "Groups.neg_le_iff_le"
   218   "REAL_LE_NEG" > "Groups.neg_le_iff_le"
   219   "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
   220   "REAL_LE_MUL" > "Rings.mult_nonneg_nonneg"
   221   "REAL_LE_LT" > "Orderings.order_le_less"
   222   "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
   223   "REAL_LE_LMUL_IMP" > "Rings.mult_mono"
   224   "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
   225   "REAL_LE_LDIV_EQ" > "Rings.pos_divide_le_eq"
   226   "REAL_LE_LDIV" > "Rings.mult_imp_div_pos_le"
   227   "REAL_LE_LADD_IMP" > "Groups.add_left_mono"
   228   "REAL_LE_LADD" > "Groups.add_le_cancel_left"
   229   "REAL_LE_INV_EQ" > "Rings.inverse_nonnegative_iff_nonnegative"
   230   "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV"
   231   "REAL_LE_DOUBLE" > "Groups.zero_le_double_add_iff_zero_le_single_add"
   232   "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"
   233   "REAL_LE_ANTISYM" > "Orderings.order_eq_iff"
   234   "REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR"
   235   "REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL"
   236   "REAL_LE_ADD2" > "Groups.add_mono"
   237   "REAL_LE_ADD" > "Groups.add_nonneg_nonneg"
   238   "REAL_LE_01" > "Rings.zero_le_one"
   239   "REAL_LET_TRANS" > "Set.basic_trans_rules_23"
   240   "REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear"
   241   "REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM"
   242   "REAL_LET_ADD2" > "Groups.add_le_less_mono"
   243   "REAL_LET_ADD" > "Groups.add_nonneg_pos"
   244   "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
   245   "REAL_LE" > "RealDef.real_of_nat_le_iff"
   246   "REAL_LDISTRIB" > "Rings.ring_eq_simps_2"
   247   "REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
   248   "REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
   249   "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
   250   "REAL_INV_LT1" > "RealDef.real_inverse_gt_one"
   251   "REAL_INV_INV" > "Rings.inverse_inverse_eq"
   252   "REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
   253   "REAL_INV_1OVER" > "Rings.inverse_eq_divide"
   254   "REAL_INV_0" > "Rings.division_by_zero_class.inverse_zero"
   255   "REAL_INVINV" > "Rings.nonzero_inverse_inverse_eq"
   256   "REAL_INV1" > "Rings.inverse_1"
   257   "REAL_INJ" > "RealDef.real_of_nat_inject"
   258   "REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
   259   "REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"
   260   "REAL_EQ_SUB_RADD" > "Rings.ring_eq_simps_15"
   261   "REAL_EQ_SUB_LADD" > "Rings.ring_eq_simps_16"
   262   "REAL_EQ_RMUL_IMP" > "Rings.field_mult_cancel_right_lemma"
   263   "REAL_EQ_RMUL" > "Rings.field_mult_cancel_right"
   264   "REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ"
   265   "REAL_EQ_RADD" > "Groups.add_right_cancel"
   266   "REAL_EQ_NEG" > "Groups.neg_equal_iff_equal"
   267   "REAL_EQ_MUL_LCANCEL" > "Rings.field_mult_cancel_left"
   268   "REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP"
   269   "REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel"
   270   "REAL_EQ_LMUL" > "Rings.field_mult_cancel_left"
   271   "REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ"
   272   "REAL_EQ_LADD" > "Groups.add_left_cancel"
   273   "REAL_EQ_IMP_LE" > "Orderings.order_eq_refl"
   274   "REAL_ENTIRE" > "Rings.field_mult_eq_0_iff"
   275   "REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
   276   "REAL_DOWN" > "HOL4Real.real.REAL_DOWN"
   277   "REAL_DOUBLE" > "Int.mult_2"
   278   "REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
   279   "REAL_DIV_REFL" > "Rings.divide_self"
   280   "REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
   281   "REAL_DIV_LZERO" > "Rings.divide_zero_left"
   282   "REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL"
   283   "REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
   284   "REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
   285   "REAL_ARCH" > "RComplete.reals_Archimedean3"
   286   "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
   287   "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
   288   "REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB"
   289   "REAL_ADD_RINV" > "Groups.right_minus"
   290   "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
   291   "REAL_ADD_RID" > "Finite_Set.AC_add.f_e.ident"
   292   "REAL_ADD_RDISTRIB" > "Rings.ring_eq_simps_1"
   293   "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   294   "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
   295   "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
   296   "REAL_ADD_LDISTRIB" > "Rings.ring_eq_simps_2"
   297   "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
   298   "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
   299   "REAL_ADD" > "RealDef.real_of_nat_add"
   300   "REAL_ABS_TRIANGLE" > "Groups.abs_triangle_ineq"
   301   "REAL_ABS_POS" > "Groups.abs_ge_zero"
   302   "REAL_ABS_MUL" > "Rings.abs_mult"
   303   "REAL_ABS_0" > "Int.bin_arith_simps_28"
   304   "REAL_10" > "HOL4Compat.REAL_10"
   305   "REAL_1" > "HOL4Real.real.REAL_1"
   306   "REAL_0" > "HOL4Real.real.REAL_0"
   307   "REAL" > "RealDef.real_of_nat_Suc"
   308   "POW_ZERO_EQ" > "HOL4Real.real.POW_ZERO_EQ"
   309   "POW_ZERO" > "RealPow.realpow_zero_zero"
   310   "POW_POS_LT" > "HOL4Real.real.POW_POS_LT"
   311   "POW_POS" > "Power.zero_le_power"
   312   "POW_PLUS1" > "HOL4Real.real.POW_PLUS1"
   313   "POW_ONE" > "Power.power_one"
   314   "POW_NZ" > "Power.field_power_not_zero"
   315   "POW_MUL" > "Power.power_mult_distrib"
   316   "POW_MINUS1" > "Nat_Numeral.power_minus1_even"
   317   "POW_M1" > "HOL4Real.real.POW_M1"
   318   "POW_LT" > "HOL4Real.real.POW_LT"
   319   "POW_LE" > "Power.power_mono"
   320   "POW_INV" > "Power.nonzero_power_inverse"
   321   "POW_EQ" > "Power.power_inject_base"
   322   "POW_ADD" > "Power.power_add"
   323   "POW_ABS" > "Power.power_abs"
   324   "POW_2_LT" > "RealPow.two_realpow_gt"
   325   "POW_2_LE1" > "RealPow.two_realpow_ge_one"
   326   "POW_2" > "Nat_Numeral.power2_eq_square"
   327   "POW_1" > "Power.power_one_right"
   328   "POW_0" > "Power.power_0_Suc"
   329   "ABS_ZERO" > "Groups.abs_eq_0"
   330   "ABS_TRIANGLE" > "Groups.abs_triangle_ineq"
   331   "ABS_SUM" > "HOL4Real.real.ABS_SUM"
   332   "ABS_SUB_ABS" > "Groups.abs_triangle_ineq3"
   333   "ABS_SUB" > "Groups.abs_minus_commute"
   334   "ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ"
   335   "ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
   336   "ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
   337   "ABS_REFL" > "HOL4Real.real.ABS_REFL"
   338   "ABS_POW2" > "Nat_Numeral.abs_power2"
   339   "ABS_POS" > "Groups.abs_ge_zero"
   340   "ABS_NZ" > "Groups.zero_less_abs_iff"
   341   "ABS_NEG" > "Groups.abs_minus_cancel"
   342   "ABS_N" > "RealDef.abs_real_of_nat_cancel"
   343   "ABS_MUL" > "Rings.abs_mult"
   344   "ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2"
   345   "ABS_LE" > "Groups.abs_ge_self"
   346   "ABS_INV" > "Rings.nonzero_abs_inverse"
   347   "ABS_DIV" > "Rings.nonzero_abs_divide"
   348   "ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE"
   349   "ABS_CASES" > "HOL4Real.real.ABS_CASES"
   350   "ABS_BOUNDS" > "RealDef.abs_le_interval_iff"
   351   "ABS_BOUND" > "HOL4Real.real.ABS_BOUND"
   352   "ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2"
   353   "ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
   354   "ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
   355   "ABS_ABS" > "Groups.abs_idempotent"
   356   "ABS_1" > "Int.bin_arith_simps_29"
   357   "ABS_0" > "Int.bin_arith_simps_28"
   358 
   359 end