src/HOL/Import/HOL/transc.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "tdiv" > "tdiv_def"
skalberg@14516
     7
  "tan" > "tan_def"
skalberg@14516
     8
  "sqrt" > "sqrt_def"
skalberg@14516
     9
  "sin" > "sin_def"
skalberg@14516
    10
  "rsum" > "rsum_def"
skalberg@14516
    11
  "root" > "root_def"
skalberg@14516
    12
  "pi" > "pi_def"
skalberg@14516
    13
  "ln" > "ln_def"
skalberg@14516
    14
  "gauge" > "gauge_def"
skalberg@14516
    15
  "fine" > "fine_def"
skalberg@14516
    16
  "exp" > "exp_def"
skalberg@14516
    17
  "dsize" > "dsize_def"
skalberg@14516
    18
  "division" > "division_def"
skalberg@14516
    19
  "cos" > "cos_def"
skalberg@14516
    20
  "atn" > "atn_def"
skalberg@14516
    21
  "asn" > "asn_def"
skalberg@14516
    22
  "acs" > "acs_def"
skalberg@14516
    23
  "Dint" > "Dint_def"
skalberg@14516
    24
skalberg@14516
    25
const_maps
skalberg@14516
    26
  "tdiv" > "HOL4Real.transc.tdiv"
skalberg@14516
    27
  "tan" > "HOL4Real.transc.tan"
skalberg@14516
    28
  "sqrt" > "HOL4Real.transc.sqrt"
skalberg@14516
    29
  "sin" > "HOL4Real.transc.sin"
skalberg@14516
    30
  "rsum" > "HOL4Real.transc.rsum"
skalberg@14516
    31
  "root" > "HOL4Real.transc.root"
skalberg@14516
    32
  "pi" > "HOL4Real.transc.pi"
skalberg@14516
    33
  "ln" > "HOL4Real.transc.ln"
skalberg@14516
    34
  "gauge" > "HOL4Real.transc.gauge"
skalberg@14516
    35
  "fine" > "HOL4Real.transc.fine"
skalberg@14516
    36
  "exp" > "HOL4Real.transc.exp"
skalberg@14516
    37
  "dsize" > "HOL4Real.transc.dsize"
skalberg@14516
    38
  "division" > "HOL4Real.transc.division"
skalberg@14516
    39
  "cos" > "HOL4Real.transc.cos"
skalberg@14516
    40
  "atn" > "HOL4Real.transc.atn"
skalberg@14516
    41
  "asn" > "HOL4Real.transc.asn"
skalberg@14516
    42
  "acs" > "HOL4Real.transc.acs"
skalberg@14516
    43
  "Dint" > "HOL4Real.transc.Dint"
skalberg@14516
    44
skalberg@14516
    45
thm_maps
skalberg@14516
    46
  "tdiv_def" > "HOL4Real.transc.tdiv_def"
skalberg@14516
    47
  "tdiv" > "HOL4Real.transc.tdiv"
skalberg@14516
    48
  "tan_def" > "HOL4Real.transc.tan_def"
skalberg@14516
    49
  "tan" > "HOL4Real.transc.tan"
skalberg@14516
    50
  "sqrt_def" > "HOL4Real.transc.sqrt_def"
skalberg@14516
    51
  "sqrt" > "HOL4Real.transc.sqrt"
skalberg@14516
    52
  "sin_def" > "HOL4Real.transc.sin_def"
skalberg@14516
    53
  "sin" > "HOL4Real.transc.sin"
skalberg@14516
    54
  "rsum_def" > "HOL4Real.transc.rsum_def"
skalberg@14516
    55
  "rsum" > "HOL4Real.transc.rsum"
skalberg@14516
    56
  "root_def" > "HOL4Real.transc.root_def"
skalberg@14516
    57
  "root" > "HOL4Real.transc.root"
skalberg@14516
    58
  "pi_def" > "HOL4Real.transc.pi_def"
skalberg@14516
    59
  "pi" > "HOL4Real.transc.pi"
skalberg@14516
    60
  "ln_def" > "HOL4Real.transc.ln_def"
skalberg@14516
    61
  "ln" > "HOL4Real.transc.ln"
skalberg@14516
    62
  "gauge_def" > "HOL4Real.transc.gauge_def"
skalberg@14516
    63
  "gauge" > "HOL4Real.transc.gauge"
skalberg@14516
    64
  "fine_def" > "HOL4Real.transc.fine_def"
skalberg@14516
    65
  "fine" > "HOL4Real.transc.fine"
skalberg@14516
    66
  "exp_def" > "HOL4Real.transc.exp_def"
skalberg@14516
    67
  "exp" > "HOL4Real.transc.exp"
skalberg@14516
    68
  "dsize_def" > "HOL4Real.transc.dsize_def"
skalberg@14516
    69
  "dsize" > "HOL4Real.transc.dsize"
skalberg@14516
    70
  "division_def" > "HOL4Real.transc.division_def"
skalberg@14516
    71
  "division" > "HOL4Real.transc.division"
skalberg@14516
    72
  "cos_def" > "HOL4Real.transc.cos_def"
skalberg@14516
    73
  "cos" > "HOL4Real.transc.cos"
skalberg@14516
    74
  "atn_def" > "HOL4Real.transc.atn_def"
skalberg@14516
    75
  "atn" > "HOL4Real.transc.atn"
skalberg@14516
    76
  "asn_def" > "HOL4Real.transc.asn_def"
skalberg@14516
    77
  "asn" > "HOL4Real.transc.asn"
skalberg@14516
    78
  "acs_def" > "HOL4Real.transc.acs_def"
skalberg@14516
    79
  "acs" > "HOL4Real.transc.acs"
skalberg@14516
    80
  "TAN_TOTAL_POS" > "HOL4Real.transc.TAN_TOTAL_POS"
skalberg@14516
    81
  "TAN_TOTAL_LEMMA" > "HOL4Real.transc.TAN_TOTAL_LEMMA"
skalberg@14516
    82
  "TAN_TOTAL" > "HOL4Real.transc.TAN_TOTAL"
skalberg@14516
    83
  "TAN_SEC" > "HOL4Real.transc.TAN_SEC"
skalberg@14516
    84
  "TAN_POS_PI2" > "HOL4Real.transc.TAN_POS_PI2"
skalberg@14516
    85
  "TAN_PI" > "HOL4Real.transc.TAN_PI"
skalberg@14516
    86
  "TAN_PERIODIC" > "HOL4Real.transc.TAN_PERIODIC"
skalberg@14516
    87
  "TAN_NPI" > "HOL4Real.transc.TAN_NPI"
skalberg@14516
    88
  "TAN_NEG" > "HOL4Real.transc.TAN_NEG"
skalberg@14516
    89
  "TAN_DOUBLE" > "HOL4Real.transc.TAN_DOUBLE"
skalberg@14516
    90
  "TAN_ATN" > "HOL4Real.transc.TAN_ATN"
skalberg@14516
    91
  "TAN_ADD" > "HOL4Real.transc.TAN_ADD"
skalberg@14516
    92
  "TAN_0" > "HOL4Real.transc.TAN_0"
skalberg@14516
    93
  "SQRT_POW_2" > "HOL4Real.transc.SQRT_POW_2"
skalberg@14516
    94
  "SQRT_POW2" > "HOL4Real.transc.SQRT_POW2"
skalberg@14516
    95
  "SQRT_POS_UNIQ" > "HOL4Real.transc.SQRT_POS_UNIQ"
skalberg@14516
    96
  "SQRT_POS_LT" > "HOL4Real.transc.SQRT_POS_LT"
skalberg@14516
    97
  "SQRT_POS_LE" > "HOL4Real.transc.SQRT_POS_LE"
skalberg@14516
    98
  "SQRT_MUL" > "HOL4Real.transc.SQRT_MUL"
skalberg@14516
    99
  "SQRT_MONO_LE" > "HOL4Real.transc.SQRT_MONO_LE"
skalberg@14516
   100
  "SQRT_INV" > "HOL4Real.transc.SQRT_INV"
skalberg@14516
   101
  "SQRT_EVEN_POW2" > "HOL4Real.transc.SQRT_EVEN_POW2"
skalberg@14516
   102
  "SQRT_EQ" > "HOL4Real.transc.SQRT_EQ"
skalberg@14516
   103
  "SQRT_DIV" > "HOL4Real.transc.SQRT_DIV"
skalberg@14516
   104
  "SQRT_1" > "HOL4Real.transc.SQRT_1"
skalberg@14516
   105
  "SQRT_0" > "HOL4Real.transc.SQRT_0"
skalberg@14516
   106
  "SIN_ZERO_LEMMA" > "HOL4Real.transc.SIN_ZERO_LEMMA"
skalberg@14516
   107
  "SIN_ZERO" > "HOL4Real.transc.SIN_ZERO"
skalberg@14516
   108
  "SIN_TOTAL" > "HOL4Real.transc.SIN_TOTAL"
skalberg@14516
   109
  "SIN_POS_PI_LE" > "HOL4Real.transc.SIN_POS_PI_LE"
skalberg@14516
   110
  "SIN_POS_PI2_LE" > "HOL4Real.transc.SIN_POS_PI2_LE"
skalberg@14516
   111
  "SIN_POS_PI2" > "HOL4Real.transc.SIN_POS_PI2"
skalberg@14516
   112
  "SIN_POS_PI" > "HOL4Real.transc.SIN_POS_PI"
skalberg@14516
   113
  "SIN_POS" > "HOL4Real.transc.SIN_POS"
skalberg@14516
   114
  "SIN_PI2" > "HOL4Real.transc.SIN_PI2"
skalberg@14516
   115
  "SIN_PI" > "HOL4Real.transc.SIN_PI"
skalberg@14516
   116
  "SIN_PERIODIC_PI" > "HOL4Real.transc.SIN_PERIODIC_PI"
skalberg@14516
   117
  "SIN_PERIODIC" > "HOL4Real.transc.SIN_PERIODIC"
skalberg@14516
   118
  "SIN_PAIRED" > "HOL4Real.transc.SIN_PAIRED"
skalberg@14516
   119
  "SIN_NPI" > "HOL4Real.transc.SIN_NPI"
skalberg@14516
   120
  "SIN_NEGLEMMA" > "HOL4Real.transc.SIN_NEGLEMMA"
skalberg@14516
   121
  "SIN_NEG" > "HOL4Real.transc.SIN_NEG"
skalberg@14516
   122
  "SIN_FDIFF" > "HOL4Real.transc.SIN_FDIFF"
skalberg@14516
   123
  "SIN_DOUBLE" > "HOL4Real.transc.SIN_DOUBLE"
skalberg@14516
   124
  "SIN_COS_SQRT" > "HOL4Real.transc.SIN_COS_SQRT"
skalberg@14516
   125
  "SIN_COS_SQ" > "HOL4Real.transc.SIN_COS_SQ"
skalberg@14516
   126
  "SIN_COS_NEG" > "HOL4Real.transc.SIN_COS_NEG"
skalberg@14516
   127
  "SIN_COS_ADD" > "HOL4Real.transc.SIN_COS_ADD"
skalberg@14516
   128
  "SIN_COS" > "HOL4Real.transc.SIN_COS"
skalberg@14516
   129
  "SIN_CONVERGES" > "HOL4Real.transc.SIN_CONVERGES"
skalberg@14516
   130
  "SIN_CIRCLE" > "HOL4Real.transc.SIN_CIRCLE"
skalberg@14516
   131
  "SIN_BOUNDS" > "HOL4Real.transc.SIN_BOUNDS"
skalberg@14516
   132
  "SIN_BOUND" > "HOL4Real.transc.SIN_BOUND"
skalberg@14516
   133
  "SIN_ASN" > "HOL4Real.transc.SIN_ASN"
skalberg@14516
   134
  "SIN_ADD" > "HOL4Real.transc.SIN_ADD"
skalberg@14516
   135
  "SIN_ACS_NZ" > "HOL4Real.transc.SIN_ACS_NZ"
skalberg@14516
   136
  "SIN_0" > "HOL4Real.transc.SIN_0"
skalberg@14516
   137
  "ROOT_POW_POS" > "HOL4Real.transc.ROOT_POW_POS"
skalberg@14516
   138
  "ROOT_POS_UNIQ" > "HOL4Real.transc.ROOT_POS_UNIQ"
skalberg@14516
   139
  "ROOT_POS_LT" > "HOL4Real.transc.ROOT_POS_LT"
skalberg@14516
   140
  "ROOT_POS" > "HOL4Real.transc.ROOT_POS"
skalberg@14516
   141
  "ROOT_MUL" > "HOL4Real.transc.ROOT_MUL"
skalberg@14516
   142
  "ROOT_MONO_LE" > "HOL4Real.transc.ROOT_MONO_LE"
skalberg@14516
   143
  "ROOT_LT_LEMMA" > "HOL4Real.transc.ROOT_LT_LEMMA"
skalberg@14516
   144
  "ROOT_LN" > "HOL4Real.transc.ROOT_LN"
skalberg@14516
   145
  "ROOT_INV" > "HOL4Real.transc.ROOT_INV"
skalberg@14516
   146
  "ROOT_DIV" > "HOL4Real.transc.ROOT_DIV"
skalberg@14516
   147
  "ROOT_1" > "HOL4Real.transc.ROOT_1"
skalberg@14516
   148
  "ROOT_0" > "HOL4Real.transc.ROOT_0"
skalberg@14516
   149
  "REAL_DIV_SQRT" > "HOL4Real.transc.REAL_DIV_SQRT"
skalberg@14516
   150
  "POW_ROOT_POS" > "HOL4Real.transc.POW_ROOT_POS"
skalberg@14516
   151
  "POW_2_SQRT" > "HOL4Real.transc.POW_2_SQRT"
skalberg@14516
   152
  "PI_POS" > "HOL4Real.transc.PI_POS"
skalberg@14516
   153
  "PI2_BOUNDS" > "HOL4Real.transc.PI2_BOUNDS"
skalberg@14516
   154
  "PI2" > "HOL4Real.transc.PI2"
skalberg@14516
   155
  "MCLAURIN_ZERO" > "HOL4Real.transc.MCLAURIN_ZERO"
skalberg@14516
   156
  "MCLAURIN_NEG" > "HOL4Real.transc.MCLAURIN_NEG"
skalberg@14516
   157
  "MCLAURIN_EXP_LT" > "HOL4Real.transc.MCLAURIN_EXP_LT"
skalberg@14516
   158
  "MCLAURIN_EXP_LE" > "HOL4Real.transc.MCLAURIN_EXP_LE"
skalberg@14516
   159
  "MCLAURIN_ALL_LT" > "HOL4Real.transc.MCLAURIN_ALL_LT"
skalberg@14516
   160
  "MCLAURIN_ALL_LE" > "HOL4Real.transc.MCLAURIN_ALL_LE"
skalberg@14516
   161
  "MCLAURIN" > "HOL4Real.transc.MCLAURIN"
skalberg@14516
   162
  "LN_POW" > "HOL4Real.transc.LN_POW"
skalberg@14516
   163
  "LN_POS" > "HOL4Real.transc.LN_POS"
skalberg@14516
   164
  "LN_MUL" > "HOL4Real.transc.LN_MUL"
skalberg@14516
   165
  "LN_MONO_LT" > "HOL4Real.transc.LN_MONO_LT"
skalberg@14516
   166
  "LN_MONO_LE" > "HOL4Real.transc.LN_MONO_LE"
skalberg@14516
   167
  "LN_LT_X" > "HOL4Real.transc.LN_LT_X"
skalberg@14516
   168
  "LN_LE" > "HOL4Real.transc.LN_LE"
skalberg@14516
   169
  "LN_INV" > "HOL4Real.transc.LN_INV"
skalberg@14516
   170
  "LN_INJ" > "HOL4Real.transc.LN_INJ"
skalberg@14516
   171
  "LN_EXP" > "HOL4Real.transc.LN_EXP"
skalberg@14516
   172
  "LN_DIV" > "HOL4Real.transc.LN_DIV"
skalberg@14516
   173
  "LN_1" > "HOL4Real.transc.LN_1"
skalberg@14516
   174
  "INTEGRAL_NULL" > "HOL4Real.transc.INTEGRAL_NULL"
skalberg@14516
   175
  "GAUGE_MIN" > "HOL4Real.transc.GAUGE_MIN"
skalberg@14516
   176
  "FTC1" > "HOL4Real.transc.FTC1"
skalberg@14516
   177
  "FINE_MIN" > "HOL4Real.transc.FINE_MIN"
skalberg@14516
   178
  "EXP_TOTAL_LEMMA" > "HOL4Real.transc.EXP_TOTAL_LEMMA"
skalberg@14516
   179
  "EXP_TOTAL" > "HOL4Real.transc.EXP_TOTAL"
skalberg@14516
   180
  "EXP_SUB" > "HOL4Real.transc.EXP_SUB"
skalberg@14516
   181
  "EXP_POS_LT" > "HOL4Real.transc.EXP_POS_LT"
skalberg@14516
   182
  "EXP_POS_LE" > "HOL4Real.transc.EXP_POS_LE"
skalberg@14516
   183
  "EXP_NZ" > "HOL4Real.transc.EXP_NZ"
skalberg@14516
   184
  "EXP_NEG_MUL2" > "HOL4Real.transc.EXP_NEG_MUL2"
skalberg@14516
   185
  "EXP_NEG_MUL" > "HOL4Real.transc.EXP_NEG_MUL"
skalberg@14516
   186
  "EXP_NEG" > "HOL4Real.transc.EXP_NEG"
skalberg@14516
   187
  "EXP_N" > "HOL4Real.transc.EXP_N"
skalberg@14516
   188
  "EXP_MONO_LT" > "HOL4Real.transc.EXP_MONO_LT"
skalberg@14516
   189
  "EXP_MONO_LE" > "HOL4Real.transc.EXP_MONO_LE"
skalberg@14516
   190
  "EXP_MONO_IMP" > "HOL4Real.transc.EXP_MONO_IMP"
skalberg@14516
   191
  "EXP_LT_1" > "HOL4Real.transc.EXP_LT_1"
skalberg@14516
   192
  "EXP_LN" > "HOL4Real.transc.EXP_LN"
skalberg@14516
   193
  "EXP_LE_X" > "HOL4Real.transc.EXP_LE_X"
skalberg@14516
   194
  "EXP_INJ" > "HOL4Real.transc.EXP_INJ"
skalberg@14516
   195
  "EXP_FDIFF" > "HOL4Real.transc.EXP_FDIFF"
skalberg@14516
   196
  "EXP_CONVERGES" > "HOL4Real.transc.EXP_CONVERGES"
skalberg@14516
   197
  "EXP_ADD_MUL" > "HOL4Real.transc.EXP_ADD_MUL"
skalberg@14516
   198
  "EXP_ADD" > "HOL4Real.transc.EXP_ADD"
skalberg@14516
   199
  "EXP_0" > "HOL4Real.transc.EXP_0"
skalberg@14516
   200
  "Dint_def" > "HOL4Real.transc.Dint_def"
skalberg@14516
   201
  "Dint" > "HOL4Real.transc.Dint"
skalberg@14516
   202
  "DIVISION_UBOUND_LT" > "HOL4Real.transc.DIVISION_UBOUND_LT"
skalberg@14516
   203
  "DIVISION_UBOUND" > "HOL4Real.transc.DIVISION_UBOUND"
skalberg@14516
   204
  "DIVISION_THM" > "HOL4Real.transc.DIVISION_THM"
skalberg@14516
   205
  "DIVISION_SINGLE" > "HOL4Real.transc.DIVISION_SINGLE"
skalberg@14516
   206
  "DIVISION_RHS" > "HOL4Real.transc.DIVISION_RHS"
skalberg@14516
   207
  "DIVISION_LT_GEN" > "HOL4Real.transc.DIVISION_LT_GEN"
skalberg@14516
   208
  "DIVISION_LT" > "HOL4Real.transc.DIVISION_LT"
skalberg@14516
   209
  "DIVISION_LHS" > "HOL4Real.transc.DIVISION_LHS"
skalberg@14516
   210
  "DIVISION_LE" > "HOL4Real.transc.DIVISION_LE"
skalberg@14516
   211
  "DIVISION_LBOUND_LT" > "HOL4Real.transc.DIVISION_LBOUND_LT"
skalberg@14516
   212
  "DIVISION_LBOUND" > "HOL4Real.transc.DIVISION_LBOUND"
skalberg@14516
   213
  "DIVISION_GT" > "HOL4Real.transc.DIVISION_GT"
skalberg@14516
   214
  "DIVISION_EXISTS" > "HOL4Real.transc.DIVISION_EXISTS"
skalberg@14516
   215
  "DIVISION_EQ" > "HOL4Real.transc.DIVISION_EQ"
skalberg@14516
   216
  "DIVISION_APPEND" > "HOL4Real.transc.DIVISION_APPEND"
skalberg@14516
   217
  "DIVISION_1" > "HOL4Real.transc.DIVISION_1"
skalberg@14516
   218
  "DIVISION_0" > "HOL4Real.transc.DIVISION_0"
skalberg@14516
   219
  "DINT_UNIQ" > "HOL4Real.transc.DINT_UNIQ"
skalberg@14516
   220
  "DIFF_TAN" > "HOL4Real.transc.DIFF_TAN"
skalberg@14516
   221
  "DIFF_SIN" > "HOL4Real.transc.DIFF_SIN"
skalberg@14516
   222
  "DIFF_LN_COMPOSITE" > "HOL4Real.transc.DIFF_LN_COMPOSITE"
skalberg@14516
   223
  "DIFF_LN" > "HOL4Real.transc.DIFF_LN"
skalberg@14516
   224
  "DIFF_EXP" > "HOL4Real.transc.DIFF_EXP"
skalberg@14516
   225
  "DIFF_COS" > "HOL4Real.transc.DIFF_COS"
skalberg@14516
   226
  "DIFF_COMPOSITE" > "HOL4Real.transc.DIFF_COMPOSITE"
skalberg@14516
   227
  "DIFF_ATN" > "HOL4Real.transc.DIFF_ATN"
skalberg@14516
   228
  "DIFF_ASN_LEMMA" > "HOL4Real.transc.DIFF_ASN_LEMMA"
skalberg@14516
   229
  "DIFF_ASN" > "HOL4Real.transc.DIFF_ASN"
skalberg@14516
   230
  "DIFF_ACS_LEMMA" > "HOL4Real.transc.DIFF_ACS_LEMMA"
skalberg@14516
   231
  "DIFF_ACS" > "HOL4Real.transc.DIFF_ACS"
skalberg@14516
   232
  "COS_ZERO_LEMMA" > "HOL4Real.transc.COS_ZERO_LEMMA"
skalberg@14516
   233
  "COS_ZERO" > "HOL4Real.transc.COS_ZERO"
skalberg@14516
   234
  "COS_TOTAL" > "HOL4Real.transc.COS_TOTAL"
skalberg@14516
   235
  "COS_SIN_SQRT" > "HOL4Real.transc.COS_SIN_SQRT"
skalberg@14516
   236
  "COS_SIN_SQ" > "HOL4Real.transc.COS_SIN_SQ"
skalberg@14516
   237
  "COS_SIN" > "HOL4Real.transc.COS_SIN"
skalberg@14516
   238
  "COS_POS_PI_LE" > "HOL4Real.transc.COS_POS_PI_LE"
skalberg@14516
   239
  "COS_POS_PI2_LE" > "HOL4Real.transc.COS_POS_PI2_LE"
skalberg@14516
   240
  "COS_POS_PI2" > "HOL4Real.transc.COS_POS_PI2"
skalberg@14516
   241
  "COS_POS_PI" > "HOL4Real.transc.COS_POS_PI"
skalberg@14516
   242
  "COS_PI2" > "HOL4Real.transc.COS_PI2"
skalberg@14516
   243
  "COS_PI" > "HOL4Real.transc.COS_PI"
skalberg@14516
   244
  "COS_PERIODIC_PI" > "HOL4Real.transc.COS_PERIODIC_PI"
skalberg@14516
   245
  "COS_PERIODIC" > "HOL4Real.transc.COS_PERIODIC"
skalberg@14516
   246
  "COS_PAIRED" > "HOL4Real.transc.COS_PAIRED"
skalberg@14516
   247
  "COS_NPI" > "HOL4Real.transc.COS_NPI"
skalberg@14516
   248
  "COS_NEG" > "HOL4Real.transc.COS_NEG"
skalberg@14516
   249
  "COS_ISZERO" > "HOL4Real.transc.COS_ISZERO"
skalberg@14516
   250
  "COS_FDIFF" > "HOL4Real.transc.COS_FDIFF"
skalberg@14516
   251
  "COS_DOUBLE" > "HOL4Real.transc.COS_DOUBLE"
skalberg@14516
   252
  "COS_CONVERGES" > "HOL4Real.transc.COS_CONVERGES"
skalberg@14516
   253
  "COS_BOUNDS" > "HOL4Real.transc.COS_BOUNDS"
skalberg@14516
   254
  "COS_BOUND" > "HOL4Real.transc.COS_BOUND"
skalberg@14516
   255
  "COS_ATN_NZ" > "HOL4Real.transc.COS_ATN_NZ"
skalberg@14516
   256
  "COS_ASN_NZ" > "HOL4Real.transc.COS_ASN_NZ"
skalberg@14516
   257
  "COS_ADD" > "HOL4Real.transc.COS_ADD"
skalberg@14516
   258
  "COS_ACS" > "HOL4Real.transc.COS_ACS"
skalberg@14516
   259
  "COS_2" > "HOL4Real.transc.COS_2"
skalberg@14516
   260
  "COS_0" > "HOL4Real.transc.COS_0"
skalberg@14516
   261
  "ATN_TAN" > "HOL4Real.transc.ATN_TAN"
skalberg@14516
   262
  "ATN_BOUNDS" > "HOL4Real.transc.ATN_BOUNDS"
skalberg@14516
   263
  "ATN" > "HOL4Real.transc.ATN"
skalberg@14516
   264
  "ASN_SIN" > "HOL4Real.transc.ASN_SIN"
skalberg@14516
   265
  "ASN_BOUNDS_LT" > "HOL4Real.transc.ASN_BOUNDS_LT"
skalberg@14516
   266
  "ASN_BOUNDS" > "HOL4Real.transc.ASN_BOUNDS"
skalberg@14516
   267
  "ASN" > "HOL4Real.transc.ASN"
skalberg@14516
   268
  "ACS_COS" > "HOL4Real.transc.ACS_COS"
skalberg@14516
   269
  "ACS_BOUNDS_LT" > "HOL4Real.transc.ACS_BOUNDS_LT"
skalberg@14516
   270
  "ACS_BOUNDS" > "HOL4Real.transc.ACS_BOUNDS"
skalberg@14516
   271
  "ACS" > "HOL4Real.transc.ACS"
skalberg@14516
   272
skalberg@14516
   273
end