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