src/HOL/Import/HOL/arithmetic.imp
author nipkow
Wed Jun 24 09:41:14 2009 +0200 (2009-06-24)
changeset 31790 05c92381363c
parent 30925 c38cbc0ac8d1
child 33657 a4179bf442d1
permissions -rw-r--r--
corrected and unified thm names
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "nat_elim__magic" > "nat_elim__magic_def"
skalberg@14516
     7
  "ODD" > "ODD_def"
skalberg@14516
     8
  "FACT" > "FACT_def"
skalberg@14516
     9
  "EVEN" > "EVEN_def"
skalberg@14516
    10
skalberg@14516
    11
const_maps
skalberg@14516
    12
  "num_case" > "Nat.nat.nat_case"
skalberg@14516
    13
  "nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic"
skalberg@14516
    14
  "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
skalberg@14516
    15
  "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
skalberg@14516
    16
  "NUMERAL" > "HOL4Compat.NUMERAL"
haftmann@23132
    17
  "MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
haftmann@23132
    18
  "MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
skalberg@14516
    19
  "FUNPOW" > "HOL4Compat.FUNPOW"
haftmann@24996
    20
  "EXP" > "Power.power_class.power" :: "nat => nat => nat"
haftmann@22997
    21
  "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
haftmann@22997
    22
  "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
skalberg@14516
    23
  "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
skalberg@14516
    24
  ">=" > "HOL4Compat.nat_ge"
skalberg@14516
    25
  ">" > "HOL4Compat.nat_gt"
haftmann@23881
    26
  "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
haftmann@22997
    27
  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
haftmann@22997
    28
  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
haftmann@22997
    29
  "*" > "HOL.times_class.times" :: "nat => nat => nat"
skalberg@14516
    30
skalberg@14516
    31
thm_maps
skalberg@14516
    32
  "num_case_def" > "HOL4Compat.num_case_def"
skalberg@14516
    33
  "num_case_cong" > "HOL4Base.arithmetic.num_case_cong"
skalberg@14516
    34
  "num_case_compute" > "HOL4Base.arithmetic.num_case_compute"
skalberg@14516
    35
  "num_CASES" > "Nat.nat.nchotomy"
skalberg@14516
    36
  "nat_elim__magic_def" > "HOL4Base.arithmetic.nat_elim__magic_def"
skalberg@14516
    37
  "nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic"
skalberg@14516
    38
  "ZERO_MOD" > "HOL4Base.arithmetic.ZERO_MOD"
skalberg@14516
    39
  "ZERO_LESS_EXP" > "HOL4Base.arithmetic.ZERO_LESS_EXP"
skalberg@14516
    40
  "ZERO_LESS_EQ" > "Nat.le0"
skalberg@14516
    41
  "ZERO_DIV" > "HOL4Base.arithmetic.ZERO_DIV"
skalberg@14516
    42
  "WOP" > "HOL4Base.arithmetic.WOP"
skalberg@14516
    43
  "TWO" > "HOL4Base.arithmetic.TWO"
skalberg@14516
    44
  "TIMES2" > "NatSimprocs.nat_mult_2"
skalberg@14516
    45
  "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
nipkow@31790
    46
  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_plus1_left"
skalberg@14516
    47
  "SUC_NOT" > "Nat.nat.simps_2"
skalberg@14516
    48
  "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
skalberg@14516
    49
  "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
wenzelm@21243
    50
  "SUB_SUB" > "Nat.diff_diff_right"
skalberg@14516
    51
  "SUB_RIGHT_SUB" > "Nat.diff_diff_left"
skalberg@14516
    52
  "SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ"
skalberg@14516
    53
  "SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS"
skalberg@14516
    54
  "SUB_RIGHT_GREATER_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER_EQ"
skalberg@14516
    55
  "SUB_RIGHT_GREATER" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER"
skalberg@14516
    56
  "SUB_RIGHT_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_EQ"
skalberg@14516
    57
  "SUB_RIGHT_ADD" > "HOL4Base.arithmetic.SUB_RIGHT_ADD"
skalberg@14516
    58
  "SUB_PLUS" > "Nat.diff_diff_left"
skalberg@14516
    59
  "SUB_MONO_EQ" > "Nat.diff_Suc_Suc"
skalberg@14516
    60
  "SUB_LESS_OR" > "HOL4Base.arithmetic.SUB_LESS_OR"
skalberg@14516
    61
  "SUB_LESS_EQ_ADD" > "HOL4Base.arithmetic.SUB_LESS_EQ_ADD"
skalberg@14516
    62
  "SUB_LESS_EQ" > "Nat.diff_le_self"
skalberg@14516
    63
  "SUB_LESS_0" > "Nat.zero_less_diff"
skalberg@14516
    64
  "SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC"
skalberg@14516
    65
  "SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB"
skalberg@14516
    66
  "SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ"
wenzelm@21243
    67
  "SUB_LEFT_LESS" > "Nat.less_diff_conv"
wenzelm@21243
    68
  "SUB_LEFT_GREATER_EQ" > "Nat.le_diff_conv"
skalberg@14516
    69
  "SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER"
skalberg@14516
    70
  "SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ"
skalberg@14516
    71
  "SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD"
skalberg@14516
    72
  "SUB_EQ_EQ_0" > "HOL4Base.arithmetic.SUB_EQ_EQ_0"
skalberg@14516
    73
  "SUB_EQ_0" > "Nat.diff_is_0_eq"
skalberg@14516
    74
  "SUB_EQUAL_0" > "Nat.diff_self_eq_0"
skalberg@14516
    75
  "SUB_ELIM_THM" > "HOL4Base.arithmetic.SUB_ELIM_THM"
skalberg@14516
    76
  "SUB_CANCEL" > "HOL4Base.arithmetic.SUB_CANCEL"
skalberg@14516
    77
  "SUB_ADD" > "Nat.le_add_diff_inverse2"
skalberg@14516
    78
  "SUB_0" > "HOL4Base.arithmetic.SUB_0"
skalberg@14516
    79
  "SUB" > "HOL4Compat.SUB"
skalberg@14516
    80
  "RIGHT_SUB_DISTRIB" > "Nat.nat_distrib_3"
skalberg@14516
    81
  "RIGHT_ADD_DISTRIB" > "Nat.nat_distrib_1"
skalberg@14516
    82
  "PRE_SUC_EQ" > "HOL4Base.arithmetic.PRE_SUC_EQ"
skalberg@14516
    83
  "PRE_SUB1" > "HOL4Base.arithmetic.PRE_SUB1"
skalberg@14516
    84
  "PRE_SUB" > "HOL4Base.arithmetic.PRE_SUB"
skalberg@14516
    85
  "PRE_ELIM_THM" > "HOL4Base.arithmetic.PRE_ELIM_THM"
skalberg@14516
    86
  "OR_LESS" > "Nat.Suc_le_lessD"
skalberg@14516
    87
  "ONE" > "Nat.One_nat_def"
skalberg@14516
    88
  "ODD_OR_EVEN" > "HOL4Base.arithmetic.ODD_OR_EVEN"
skalberg@14516
    89
  "ODD_MULT" > "HOL4Base.arithmetic.ODD_MULT"
skalberg@14516
    90
  "ODD_EXISTS" > "HOL4Base.arithmetic.ODD_EXISTS"
skalberg@14516
    91
  "ODD_EVEN" > "HOL4Base.arithmetic.ODD_EVEN"
skalberg@14516
    92
  "ODD_DOUBLE" > "HOL4Base.arithmetic.ODD_DOUBLE"
skalberg@14516
    93
  "ODD_ADD" > "HOL4Base.arithmetic.ODD_ADD"
skalberg@14516
    94
  "ODD" > "HOL4Base.arithmetic.ODD"
skalberg@14516
    95
  "NUMERAL_DEF" > "HOL4Compat.NUMERAL_def"
skalberg@14516
    96
  "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2_def"
skalberg@14516
    97
  "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1_def"
skalberg@14516
    98
  "NOT_ZERO_LT_ZERO" > "Nat.neq0_conv"
skalberg@14516
    99
  "NOT_SUC_LESS_EQ_0" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ_0"
skalberg@14516
   100
  "NOT_SUC_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ"
skalberg@14516
   101
  "NOT_SUC_ADD_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_ADD_LESS_EQ"
skalberg@14516
   102
  "NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN"
skalberg@14516
   103
  "NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ"
paulson@16796
   104
  "NOT_LESS_EQUAL" > "Orderings.linorder_not_le"
obua@17188
   105
  "NOT_LESS" > "Nat.le_def"
skalberg@14516
   106
  "NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
skalberg@14516
   107
  "NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
obua@17188
   108
  "NOT_GREATER" > "Nat.le_def"
skalberg@14516
   109
  "NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
skalberg@14516
   110
  "NORM_0" > "HOL4Base.arithmetic.NORM_0"
haftmann@25930
   111
  "MULT_SYM" > "Int.zmult_ac_2"
skalberg@14516
   112
  "MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ"
skalberg@14516
   113
  "MULT_SUC" > "Nat.mult_Suc_right"
obua@17188
   114
  "MULT_RIGHT_1" > "Finite_Set.AC_mult.f_e.ident"
skalberg@14516
   115
  "MULT_MONO_EQ" > "Nat.Suc_mult_cancel1"
skalberg@14516
   116
  "MULT_LESS_EQ_SUC" > "Nat.Suc_mult_le_cancel1"
obua@17188
   117
  "MULT_LEFT_1" > "Finite_Set.AC_mult.f_e.left_ident"
skalberg@14516
   118
  "MULT_INCREASES" > "HOL4Base.arithmetic.MULT_INCREASES"
skalberg@14516
   119
  "MULT_EXP_MONO" > "HOL4Base.arithmetic.MULT_EXP_MONO"
skalberg@14516
   120
  "MULT_EQ_1" > "HOL4Base.arithmetic.MULT_EQ_1"
skalberg@14516
   121
  "MULT_EQ_0" > "Nat.mult_is_0"
skalberg@14516
   122
  "MULT_DIV" > "Divides.div_mult_self_is_m"
haftmann@25930
   123
  "MULT_COMM" > "Int.zmult_ac_2"
skalberg@14516
   124
  "MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES"
haftmann@25930
   125
  "MULT_ASSOC" > "Int.zmult_ac_1"
skalberg@14516
   126
  "MULT_0" > "Nat.mult_0_right"
skalberg@14516
   127
  "MULT" > "HOL4Compat.MULT"
skalberg@14516
   128
  "MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE"
skalberg@14516
   129
  "MOD_TIMES2" > "HOL4Base.arithmetic.MOD_TIMES2"
skalberg@14516
   130
  "MOD_TIMES" > "HOL4Base.arithmetic.MOD_TIMES"
skalberg@14516
   131
  "MOD_PLUS" > "HOL4Base.arithmetic.MOD_PLUS"
skalberg@14516
   132
  "MOD_P" > "HOL4Base.arithmetic.MOD_P"
skalberg@14516
   133
  "MOD_ONE" > "Divides.mod_1"
skalberg@14516
   134
  "MOD_MULT_MOD" > "HOL4Base.arithmetic.MOD_MULT_MOD"
skalberg@14516
   135
  "MOD_MULT" > "HOL4Base.arithmetic.MOD_MULT"
skalberg@14516
   136
  "MOD_MOD" > "HOL4Base.arithmetic.MOD_MOD"
skalberg@14516
   137
  "MOD_EQ_0" > "HOL4Base.arithmetic.MOD_EQ_0"
skalberg@14516
   138
  "MOD_COMMON_FACTOR" > "HOL4Base.arithmetic.MOD_COMMON_FACTOR"
skalberg@14516
   139
  "MIN_MAX_PRED" > "HOL4Base.arithmetic.MIN_MAX_PRED"
skalberg@14516
   140
  "MIN_MAX_LT" > "HOL4Base.arithmetic.MIN_MAX_LT"
skalberg@14516
   141
  "MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ"
skalberg@14516
   142
  "MIN_LT" > "HOL4Base.arithmetic.MIN_LT"
skalberg@14516
   143
  "MIN_LE" > "HOL4Base.arithmetic.MIN_LE"
obua@17188
   144
  "MIN_IDEM" > "Finite_Set.min.f.ACI_4"
skalberg@14516
   145
  "MIN_DEF" > "HOL4Compat.MIN_DEF"
obua@17188
   146
  "MIN_COMM" > "Finite_Set.min.f.ACI_2"
obua@17188
   147
  "MIN_ASSOC" > "Finite_Set.min.f.ACI_1"
skalberg@14516
   148
  "MIN_0" > "HOL4Base.arithmetic.MIN_0"
skalberg@14516
   149
  "MAX_LT" > "HOL4Base.arithmetic.MAX_LT"
skalberg@14516
   150
  "MAX_LE" > "HOL4Base.arithmetic.MAX_LE"
obua@17188
   151
  "MAX_IDEM" > "Finite_Set.max.f.ACI_4"
skalberg@14516
   152
  "MAX_DEF" > "HOL4Compat.MAX_DEF"
obua@17188
   153
  "MAX_COMM" > "Finite_Set.max.f.ACI_2"
obua@17188
   154
  "MAX_ASSOC" > "Finite_Set.max.f.ACI_1"
skalberg@14516
   155
  "MAX_0" > "HOL4Base.arithmetic.MAX_0"
skalberg@14516
   156
  "LESS_TRANS" > "Nat.less_trans"
skalberg@14516
   157
  "LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT"
skalberg@14516
   158
  "LESS_SUC_EQ_COR" > "Nat.Suc_lessI"
skalberg@14516
   159
  "LESS_SUB_ADD_LESS" > "HOL4Base.arithmetic.LESS_SUB_ADD_LESS"
skalberg@14516
   160
  "LESS_OR_EQ_ADD" > "HOL4Base.arithmetic.LESS_OR_EQ_ADD"
skalberg@14516
   161
  "LESS_OR_EQ" > "HOL4Compat.LESS_OR_EQ"
skalberg@14516
   162
  "LESS_OR" > "Nat.Suc_leI"
skalberg@14516
   163
  "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
skalberg@14516
   164
  "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
avigad@16775
   165
  "LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
skalberg@14516
   166
  "LESS_MONO_REV" > "Nat.Suc_less_SucD"
skalberg@14516
   167
  "LESS_MONO_MULT" > "Nat.mult_le_mono1"
skalberg@14516
   168
  "LESS_MONO_EQ" > "Nat.Suc_less_eq"
wenzelm@14796
   169
  "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
wenzelm@14796
   170
  "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
skalberg@14516
   171
  "LESS_MONO_ADD" > "Nat.add_less_mono1"
skalberg@14516
   172
  "LESS_MOD" > "Divides.mod_less"
skalberg@14516
   173
  "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
skalberg@14516
   174
  "LESS_LESS_EQ_TRANS" > "Nat.less_le_trans"
skalberg@14516
   175
  "LESS_LESS_CASES" > "HOL4Base.arithmetic.LESS_LESS_CASES"
skalberg@14516
   176
  "LESS_IMP_LESS_OR_EQ" > "Nat.le_simps_1"
skalberg@14516
   177
  "LESS_IMP_LESS_ADD" > "Nat.trans_less_add1"
skalberg@14516
   178
  "LESS_EXP_SUC_MONO" > "HOL4Base.arithmetic.LESS_EXP_SUC_MONO"
skalberg@14516
   179
  "LESS_EQ_TRANS" > "Nat.le_trans"
skalberg@14516
   180
  "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
skalberg@14516
   181
  "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
obua@17188
   182
  "LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
wenzelm@14796
   183
  "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
skalberg@14516
   184
  "LESS_EQ_MONO" > "Nat.Suc_le_mono"
skalberg@14516
   185
  "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
skalberg@14516
   186
  "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
skalberg@14516
   187
  "LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc"
wenzelm@21243
   188
  "LESS_EQ_EXISTS" > "Nat.le_iff_add"
skalberg@14516
   189
  "LESS_EQ_CASES" > "Nat.nat_le_linear"
skalberg@14516
   190
  "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
wenzelm@21243
   191
  "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
skalberg@14516
   192
  "LESS_EQ_ADD" > "Nat.le_add1"
skalberg@14516
   193
  "LESS_EQ_0" > "Nat.le_0_eq"
skalberg@14516
   194
  "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
skalberg@14516
   195
  "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
skalberg@14516
   196
  "LESS_EQ" > "Nat.le_simps_3"
skalberg@14516
   197
  "LESS_DIV_EQ_ZERO" > "Divides.div_less"
skalberg@14516
   198
  "LESS_CASES_IMP" > "HOL4Base.arithmetic.LESS_CASES_IMP"
skalberg@14516
   199
  "LESS_CASES" > "HOL4Base.arithmetic.LESS_CASES"
skalberg@14516
   200
  "LESS_ANTISYM" > "HOL4Base.arithmetic.LESS_ANTISYM"
skalberg@14516
   201
  "LESS_ADD_SUC" > "HOL4Base.arithmetic.LESS_ADD_SUC"
skalberg@14516
   202
  "LESS_ADD_NONZERO" > "HOL4Base.arithmetic.LESS_ADD_NONZERO"
skalberg@14516
   203
  "LESS_ADD_1" > "HOL4Base.arithmetic.LESS_ADD_1"
skalberg@14516
   204
  "LESS_ADD" > "HOL4Base.arithmetic.LESS_ADD"
skalberg@14516
   205
  "LESS_0_CASES" > "HOL4Base.arithmetic.LESS_0_CASES"
skalberg@14516
   206
  "LEFT_SUB_DISTRIB" > "Nat.nat_distrib_4"
skalberg@14516
   207
  "LEFT_ADD_DISTRIB" > "Nat.nat_distrib_2"
skalberg@14516
   208
  "LE" > "HOL4Base.arithmetic.LE"
skalberg@14516
   209
  "INV_PRE_LESS_EQ" > "HOL4Base.arithmetic.INV_PRE_LESS_EQ"
skalberg@14516
   210
  "INV_PRE_LESS" > "HOL4Base.arithmetic.INV_PRE_LESS"
skalberg@14516
   211
  "INV_PRE_EQ" > "HOL4Base.arithmetic.INV_PRE_EQ"
skalberg@14516
   212
  "GREATER_OR_EQ" > "HOL4Compat.GREATER_OR_EQ"
skalberg@14516
   213
  "GREATER_EQ" > "HOL4Compat.real_ge"
skalberg@14516
   214
  "GREATER_DEF" > "HOL4Compat.GREATER_DEF"
skalberg@14516
   215
  "FUN_EQ_LEMMA" > "HOL4Base.arithmetic.FUN_EQ_LEMMA"
skalberg@14516
   216
  "FUNPOW" > "HOL4Compat.FUNPOW"
skalberg@14516
   217
  "FACT_LESS" > "HOL4Base.arithmetic.FACT_LESS"
skalberg@14516
   218
  "FACT" > "HOL4Base.arithmetic.FACT"
skalberg@14516
   219
  "EXP_INJECTIVE" > "Power.power_inject_exp"
skalberg@14516
   220
  "EXP_EQ_1" > "HOL4Base.arithmetic.EXP_EQ_1"
skalberg@14516
   221
  "EXP_EQ_0" > "HOL4Base.arithmetic.EXP_EQ_0"
skalberg@14516
   222
  "EXP_ALWAYS_BIG_ENOUGH" > "HOL4Base.arithmetic.EXP_ALWAYS_BIG_ENOUGH"
skalberg@14516
   223
  "EXP_ADD" > "Power.power_add"
skalberg@14516
   224
  "EXP_1" > "HOL4Base.arithmetic.EXP_1"
skalberg@14516
   225
  "EXP" > "HOL4Compat.EXP"
skalberg@14516
   226
  "EXISTS_GREATEST" > "HOL4Base.arithmetic.EXISTS_GREATEST"
skalberg@14516
   227
  "EVEN_OR_ODD" > "HOL4Base.arithmetic.EVEN_OR_ODD"
skalberg@14516
   228
  "EVEN_ODD_EXISTS" > "HOL4Base.arithmetic.EVEN_ODD_EXISTS"
skalberg@14516
   229
  "EVEN_ODD" > "HOL4Base.arithmetic.EVEN_ODD"
skalberg@14516
   230
  "EVEN_MULT" > "HOL4Base.arithmetic.EVEN_MULT"
skalberg@14516
   231
  "EVEN_EXISTS" > "HOL4Base.arithmetic.EVEN_EXISTS"
skalberg@14516
   232
  "EVEN_DOUBLE" > "HOL4Base.arithmetic.EVEN_DOUBLE"
skalberg@14516
   233
  "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
skalberg@14516
   234
  "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
skalberg@14516
   235
  "EVEN" > "HOL4Base.arithmetic.EVEN"
haftmann@30925
   236
  "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
skalberg@14516
   237
  "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
skalberg@15647
   238
  "EQ_LESS_EQ" > "Orderings.order_eq_iff"
skalberg@14516
   239
  "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
skalberg@14516
   240
  "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
skalberg@14516
   241
  "DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE"
skalberg@14516
   242
  "DIV_P" > "HOL4Base.arithmetic.DIV_P"
skalberg@14516
   243
  "DIV_ONE" > "Divides.div_1"
skalberg@14516
   244
  "DIV_MULT" > "HOL4Base.arithmetic.DIV_MULT"
skalberg@14516
   245
  "DIV_LESS_EQ" > "HOL4Base.arithmetic.DIV_LESS_EQ"
skalberg@14516
   246
  "DIV_LESS" > "Divides.div_less_dividend"
skalberg@14516
   247
  "DIV_DIV_DIV_MULT" > "HOL4Base.arithmetic.DIV_DIV_DIV_MULT"
skalberg@14516
   248
  "DIVMOD_ID" > "HOL4Base.arithmetic.DIVMOD_ID"
skalberg@14516
   249
  "DIVISION" > "HOL4Compat.DIVISION"
skalberg@14516
   250
  "DA" > "HOL4Base.arithmetic.DA"
skalberg@14516
   251
  "COMPLETE_INDUCTION" > "Nat.less_induct"
wenzelm@21243
   252
  "CANCEL_SUB" > "Nat.eq_diff_iff"
skalberg@14516
   253
  "ALT_ZERO" > "HOL4Compat.ALT_ZERO_def"
obua@17188
   254
  "ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
skalberg@14516
   255
  "ADD_SUC" > "Nat.add_Suc_right"
skalberg@14516
   256
  "ADD_SUB" > "Nat.diff_add_inverse2"
skalberg@14516
   257
  "ADD_MONO_LESS_EQ" > "Nat.nat_add_left_cancel_le"
skalberg@14516
   258
  "ADD_INV_0_EQ" > "HOL4Base.arithmetic.ADD_INV_0_EQ"
skalberg@14516
   259
  "ADD_INV_0" > "Nat.add_eq_self_zero"
skalberg@14516
   260
  "ADD_EQ_SUB" > "HOL4Base.arithmetic.ADD_EQ_SUB"
skalberg@14516
   261
  "ADD_EQ_1" > "HOL4Base.arithmetic.ADD_EQ_1"
skalberg@14516
   262
  "ADD_EQ_0" > "Nat.add_is_0"
skalberg@14516
   263
  "ADD_DIV_ADD_DIV" > "HOL4Base.arithmetic.ADD_DIV_ADD_DIV"
obua@17188
   264
  "ADD_COMM" > "Finite_Set.AC_add.f.AC_2"
skalberg@14516
   265
  "ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
obua@17188
   266
  "ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
obua@17188
   267
  "ADD_0" > "Finite_Set.AC_add.f_e.ident"
nipkow@31790
   268
  "ADD1" > "Nat_Numeral.Suc_eq_plus1"
skalberg@14516
   269
  "ADD" > "HOL4Compat.ADD"
skalberg@14516
   270
skalberg@14516
   271
end