src/HOL/Import/HOL/word32.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 44763 b50d5d694838
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
  "word_suc" > "word_suc_def"
skalberg@14516
     7
  "word_sub" > "word_sub_def"
skalberg@14516
     8
  "word_ror1" > "word_ror1_def"
skalberg@14516
     9
  "word_ror" > "word_ror_def"
skalberg@14516
    10
  "word_mul" > "word_mul_def"
skalberg@14516
    11
  "word_lsr1" > "word_lsr1_def"
skalberg@14516
    12
  "word_lsr" > "word_lsr_def"
skalberg@14516
    13
  "word_lsl" > "word_lsl_def"
skalberg@14516
    14
  "word_asr1" > "word_asr1_def"
skalberg@14516
    15
  "word_asr" > "word_asr_def"
skalberg@14516
    16
  "word_add" > "word_add_def"
skalberg@14516
    17
  "word_2comp" > "word_2comp_def"
skalberg@14516
    18
  "word_1comp" > "word_1comp_def"
skalberg@14516
    19
  "w_T" > "w_T_primdef"
skalberg@14516
    20
  "w_1" > "w_1_primdef"
skalberg@14516
    21
  "w_0" > "w_0_primdef"
skalberg@14516
    22
  "w2n" > "w2n_primdef"
skalberg@14516
    23
  "n2w" > "n2w_primdef"
skalberg@14516
    24
  "mk_word32" > "mk_word32_def"
skalberg@14516
    25
  "dest_word32" > "dest_word32_def"
skalberg@14516
    26
  "bitwise_or" > "bitwise_or_def"
skalberg@14516
    27
  "bitwise_eor" > "bitwise_eor_def"
skalberg@14516
    28
  "bitwise_and" > "bitwise_and_def"
skalberg@14516
    29
  "WL" > "WL_primdef"
skalberg@14516
    30
  "TWO_COMP" > "TWO_COMP_primdef"
skalberg@14516
    31
  "TOw" > "TOw_primdef"
skalberg@14516
    32
  "SLICEw" > "SLICEw_primdef"
skalberg@14516
    33
  "RRXn" > "RRXn_primdef"
skalberg@14516
    34
  "RRX" > "RRX_primdef"
skalberg@14516
    35
  "ROR_ONE" > "ROR_ONE_primdef"
skalberg@14516
    36
  "OR" > "OR_primdef"
skalberg@14516
    37
  "ONE_COMP" > "ONE_COMP_primdef"
skalberg@14516
    38
  "MSBn" > "MSBn_primdef"
skalberg@14516
    39
  "MSB" > "MSB_primdef"
skalberg@14516
    40
  "MODw" > "MODw_primdef"
skalberg@14516
    41
  "LSR_ONE" > "LSR_ONE_primdef"
skalberg@14516
    42
  "LSB" > "LSB_primdef"
skalberg@14516
    43
  "INw" > "INw_primdef"
skalberg@14516
    44
  "HB" > "HB_primdef"
skalberg@14516
    45
  "EQUIV" > "EQUIV_primdef"
skalberg@14516
    46
  "EOR" > "EOR_primdef"
skalberg@14516
    47
  "COMP0" > "COMP0_primdef"
skalberg@14516
    48
  "BITw" > "BITw_primdef"
skalberg@14516
    49
  "BITSw" > "BITSw_primdef"
skalberg@14516
    50
  "ASR_ONE" > "ASR_ONE_primdef"
skalberg@14516
    51
  "AONE" > "AONE_primdef"
skalberg@14516
    52
  "AND" > "AND_primdef"
skalberg@14516
    53
skalberg@14516
    54
type_maps
skalberg@14516
    55
  "word32" > "HOL4Word32.word32.word32"
skalberg@14516
    56
skalberg@14516
    57
const_maps
skalberg@14516
    58
  "word_suc" > "HOL4Word32.word32.word_suc"
skalberg@14516
    59
  "word_sub" > "HOL4Word32.word32.word_sub"
skalberg@14516
    60
  "word_ror1" > "HOL4Word32.word32.word_ror1"
skalberg@14516
    61
  "word_ror" > "HOL4Word32.word32.word_ror"
skalberg@14516
    62
  "word_mul" > "HOL4Word32.word32.word_mul"
skalberg@14516
    63
  "word_lsr1" > "HOL4Word32.word32.word_lsr1"
skalberg@14516
    64
  "word_lsr" > "HOL4Word32.word32.word_lsr"
skalberg@14516
    65
  "word_lsl" > "HOL4Word32.word32.word_lsl"
skalberg@14516
    66
  "word_asr1" > "HOL4Word32.word32.word_asr1"
skalberg@14516
    67
  "word_asr" > "HOL4Word32.word32.word_asr"
skalberg@14516
    68
  "word_add" > "HOL4Word32.word32.word_add"
skalberg@14516
    69
  "word_2comp" > "HOL4Word32.word32.word_2comp"
skalberg@14516
    70
  "word_1comp" > "HOL4Word32.word32.word_1comp"
skalberg@14516
    71
  "w_T" > "HOL4Word32.word32.w_T"
skalberg@14516
    72
  "w_1" > "HOL4Word32.word32.w_1"
skalberg@14516
    73
  "w_0" > "HOL4Word32.word32.w_0"
skalberg@14516
    74
  "w2n" > "HOL4Word32.word32.w2n"
skalberg@14516
    75
  "n2w" > "HOL4Word32.word32.n2w"
skalberg@14516
    76
  "bitwise_or" > "HOL4Word32.word32.bitwise_or"
skalberg@14516
    77
  "bitwise_eor" > "HOL4Word32.word32.bitwise_eor"
skalberg@14516
    78
  "bitwise_and" > "HOL4Word32.word32.bitwise_and"
skalberg@14516
    79
  "WL" > "HOL4Word32.word32.WL"
skalberg@14516
    80
  "TWO_COMP" > "HOL4Word32.word32.TWO_COMP"
skalberg@14516
    81
  "TOw" > "HOL4Word32.word32.TOw"
skalberg@14516
    82
  "SLICEw" > "HOL4Word32.word32.SLICEw"
skalberg@14516
    83
  "RRXn" > "HOL4Word32.word32.RRXn"
skalberg@14516
    84
  "RRX" > "HOL4Word32.word32.RRX"
skalberg@14516
    85
  "ROR_ONE" > "HOL4Word32.word32.ROR_ONE"
skalberg@14516
    86
  "OR" > "HOL4Word32.word32.OR"
skalberg@14516
    87
  "ONE_COMP" > "HOL4Word32.word32.ONE_COMP"
skalberg@14516
    88
  "MSBn" > "HOL4Word32.word32.MSBn"
skalberg@14516
    89
  "MSB" > "HOL4Word32.word32.MSB"
skalberg@14516
    90
  "MODw" > "HOL4Word32.word32.MODw"
skalberg@14516
    91
  "LSR_ONE" > "HOL4Word32.word32.LSR_ONE"
skalberg@14516
    92
  "LSB" > "HOL4Word32.word32.LSB"
skalberg@14516
    93
  "INw" > "HOL4Word32.word32.INw"
skalberg@14516
    94
  "HB" > "HOL4Word32.word32.HB"
skalberg@14516
    95
  "EQUIV" > "HOL4Word32.word32.EQUIV"
skalberg@14516
    96
  "EOR" > "HOL4Word32.word32.EOR"
skalberg@14516
    97
  "COMP0" > "HOL4Word32.word32.COMP0"
skalberg@14516
    98
  "BITw" > "HOL4Word32.word32.BITw"
skalberg@14516
    99
  "BITSw" > "HOL4Word32.word32.BITSw"
skalberg@14516
   100
  "ASR_ONE" > "HOL4Word32.word32.ASR_ONE"
skalberg@14516
   101
  "AONE" > "HOL4Word32.word32.AONE"
skalberg@14516
   102
  "AND" > "HOL4Word32.word32.AND"
skalberg@14516
   103
skalberg@14516
   104
const_renames
skalberg@14516
   105
  "==" > "EQUIV"
skalberg@14516
   106
skalberg@14516
   107
thm_maps
skalberg@14516
   108
  "word_suc_def" > "HOL4Word32.word32.word_suc_def"
skalberg@14516
   109
  "word_suc" > "HOL4Word32.word32.word_suc"
skalberg@14516
   110
  "word_sub_def" > "HOL4Word32.word32.word_sub_def"
skalberg@14516
   111
  "word_sub" > "HOL4Word32.word32.word_sub"
skalberg@14516
   112
  "word_ror_def" > "HOL4Word32.word32.word_ror_def"
skalberg@14516
   113
  "word_ror1_def" > "HOL4Word32.word32.word_ror1_def"
skalberg@14516
   114
  "word_ror1" > "HOL4Word32.word32.word_ror1"
skalberg@14516
   115
  "word_ror" > "HOL4Word32.word32.word_ror"
skalberg@14516
   116
  "word_nchotomy" > "HOL4Word32.word32.word_nchotomy"
skalberg@14516
   117
  "word_mul_def" > "HOL4Word32.word32.word_mul_def"
skalberg@14516
   118
  "word_mul" > "HOL4Word32.word32.word_mul"
skalberg@14516
   119
  "word_lsr_def" > "HOL4Word32.word32.word_lsr_def"
skalberg@14516
   120
  "word_lsr1_def" > "HOL4Word32.word32.word_lsr1_def"
skalberg@14516
   121
  "word_lsr1" > "HOL4Word32.word32.word_lsr1"
skalberg@14516
   122
  "word_lsr" > "HOL4Word32.word32.word_lsr"
skalberg@14516
   123
  "word_lsl_def" > "HOL4Word32.word32.word_lsl_def"
skalberg@14516
   124
  "word_lsl" > "HOL4Word32.word32.word_lsl"
skalberg@14516
   125
  "word_asr_def" > "HOL4Word32.word32.word_asr_def"
skalberg@14516
   126
  "word_asr1_def" > "HOL4Word32.word32.word_asr1_def"
skalberg@14516
   127
  "word_asr1" > "HOL4Word32.word32.word_asr1"
skalberg@14516
   128
  "word_asr" > "HOL4Word32.word32.word_asr"
skalberg@14516
   129
  "word_add_def" > "HOL4Word32.word32.word_add_def"
skalberg@14516
   130
  "word_add" > "HOL4Word32.word32.word_add"
skalberg@14516
   131
  "word_2comp_def" > "HOL4Word32.word32.word_2comp_def"
skalberg@14516
   132
  "word_2comp" > "HOL4Word32.word32.word_2comp"
skalberg@14516
   133
  "word_1comp_def" > "HOL4Word32.word32.word_1comp_def"
skalberg@14516
   134
  "word_1comp" > "HOL4Word32.word32.word_1comp"
skalberg@14516
   135
  "word32_tybij" > "HOL4Word32.word32.word32_tybij"
skalberg@14516
   136
  "word32_TY_DEF" > "HOL4Word32.word32.word32_TY_DEF"
skalberg@14516
   137
  "w_T_primdef" > "HOL4Word32.word32.w_T_primdef"
skalberg@14516
   138
  "w_T_def" > "HOL4Word32.word32.w_T_def"
skalberg@14516
   139
  "w_T" > "HOL4Word32.word32.w_T"
skalberg@14516
   140
  "w_1_primdef" > "HOL4Word32.word32.w_1_primdef"
skalberg@14516
   141
  "w_1_def" > "HOL4Word32.word32.w_1_def"
skalberg@14516
   142
  "w_1" > "HOL4Word32.word32.w_1"
skalberg@14516
   143
  "w_0_primdef" > "HOL4Word32.word32.w_0_primdef"
skalberg@14516
   144
  "w_0_def" > "HOL4Word32.word32.w_0_def"
skalberg@14516
   145
  "w_0" > "HOL4Word32.word32.w_0"
skalberg@14516
   146
  "w2n_primdef" > "HOL4Word32.word32.w2n_primdef"
skalberg@14516
   147
  "w2n_def" > "HOL4Word32.word32.w2n_def"
skalberg@14516
   148
  "w2n_EVAL" > "HOL4Word32.word32.w2n_EVAL"
skalberg@14516
   149
  "w2n_ELIM" > "HOL4Word32.word32.w2n_ELIM"
skalberg@14516
   150
  "n2w_primdef" > "HOL4Word32.word32.n2w_primdef"
skalberg@14516
   151
  "n2w_def" > "HOL4Word32.word32.n2w_def"
skalberg@14516
   152
  "n2w_11" > "HOL4Word32.word32.n2w_11"
skalberg@14516
   153
  "dest_word_mk_word_eq3" > "HOL4Word32.word32.dest_word_mk_word_eq3"
skalberg@14516
   154
  "bitwise_or_def" > "HOL4Word32.word32.bitwise_or_def"
skalberg@14516
   155
  "bitwise_or" > "HOL4Word32.word32.bitwise_or"
skalberg@14516
   156
  "bitwise_eor_def" > "HOL4Word32.word32.bitwise_eor_def"
skalberg@14516
   157
  "bitwise_eor" > "HOL4Word32.word32.bitwise_eor"
skalberg@14516
   158
  "bitwise_and_def" > "HOL4Word32.word32.bitwise_and_def"
skalberg@14516
   159
  "bitwise_and" > "HOL4Word32.word32.bitwise_and"
skalberg@14516
   160
  "ZERO_SHIFT2" > "HOL4Word32.word32.ZERO_SHIFT2"
skalberg@14516
   161
  "ZERO_SHIFT" > "HOL4Word32.word32.ZERO_SHIFT"
skalberg@14516
   162
  "WL_primdef" > "HOL4Word32.word32.WL_primdef"
skalberg@14516
   163
  "WL_def" > "HOL4Word32.word32.WL_def"
skalberg@14516
   164
  "TWO_COMP_primdef" > "HOL4Word32.word32.TWO_COMP_primdef"
skalberg@14516
   165
  "TWO_COMP_def" > "HOL4Word32.word32.TWO_COMP_def"
skalberg@14516
   166
  "TWO_COMP_WELLDEF" > "HOL4Word32.word32.TWO_COMP_WELLDEF"
skalberg@14516
   167
  "TWO_COMP_ONE_COMP_QT" > "HOL4Word32.word32.TWO_COMP_ONE_COMP_QT"
skalberg@14516
   168
  "TWO_COMP_ONE_COMP" > "HOL4Word32.word32.TWO_COMP_ONE_COMP"
skalberg@14516
   169
  "TWO_COMP_EVAL2" > "HOL4Word32.word32.TWO_COMP_EVAL2"
skalberg@14516
   170
  "TWO_COMP_EVAL" > "HOL4Word32.word32.TWO_COMP_EVAL"
skalberg@14516
   171
  "TWO_COMP_ELIM" > "HOL4Word32.word32.TWO_COMP_ELIM"
skalberg@14516
   172
  "TWO_COMP_ADD" > "HOL4Word32.word32.TWO_COMP_ADD"
skalberg@14516
   173
  "TOw_primdef" > "HOL4Word32.word32.TOw_primdef"
skalberg@14516
   174
  "TOw_def" > "HOL4Word32.word32.TOw_def"
skalberg@14516
   175
  "TOw_WELLDEF" > "HOL4Word32.word32.TOw_WELLDEF"
skalberg@14516
   176
  "TOw_QT" > "HOL4Word32.word32.TOw_QT"
skalberg@14516
   177
  "TOw_IDEM" > "HOL4Word32.word32.TOw_IDEM"
skalberg@14516
   178
  "SUC_WELLDEF" > "HOL4Word32.word32.SUC_WELLDEF"
skalberg@14516
   179
  "SUC_EQUIV_COMP" > "HOL4Word32.word32.SUC_EQUIV_COMP"
skalberg@14516
   180
  "SUBw" > "HOL4Word32.word32.SUBw"
skalberg@14516
   181
  "SUB_SUBw" > "HOL4Word32.word32.SUB_SUBw"
skalberg@14516
   182
  "SUB_PLUSw" > "HOL4Word32.word32.SUB_PLUSw"
skalberg@14516
   183
  "SUB_EQUALw" > "HOL4Word32.word32.SUB_EQUALw"
skalberg@14516
   184
  "SLICEw_primdef" > "HOL4Word32.word32.SLICEw_primdef"
skalberg@14516
   185
  "SLICEw_def" > "HOL4Word32.word32.SLICEw_def"
skalberg@14516
   186
  "SLICEw_ZERO_THM" > "HOL4Word32.word32.SLICEw_ZERO_THM"
skalberg@14516
   187
  "SLICEw_ZERO" > "HOL4Word32.word32.SLICEw_ZERO"
skalberg@14516
   188
  "SLICEw_THM" > "HOL4Word32.word32.SLICEw_THM"
skalberg@14516
   189
  "SLICEw_COMP_THM" > "HOL4Word32.word32.SLICEw_COMP_THM"
skalberg@14516
   190
  "SLICE_EVAL" > "HOL4Word32.word32.SLICE_EVAL"
skalberg@14516
   191
  "RRXn_primdef" > "HOL4Word32.word32.RRXn_primdef"
skalberg@14516
   192
  "RRXn_def" > "HOL4Word32.word32.RRXn_def"
skalberg@14516
   193
  "RRX_primdef" > "HOL4Word32.word32.RRX_primdef"
skalberg@14516
   194
  "RRX_def" > "HOL4Word32.word32.RRX_def"
skalberg@14516
   195
  "RRX_WELLDEF" > "HOL4Word32.word32.RRX_WELLDEF"
skalberg@14516
   196
  "RRX_EVAL2" > "HOL4Word32.word32.RRX_EVAL2"
skalberg@14516
   197
  "RRX_EVAL" > "HOL4Word32.word32.RRX_EVAL"
skalberg@14516
   198
  "ROR_w_T" > "HOL4Word32.word32.ROR_w_T"
skalberg@14516
   199
  "ROR_THM" > "HOL4Word32.word32.ROR_THM"
skalberg@14516
   200
  "ROR_ONE_primdef" > "HOL4Word32.word32.ROR_ONE_primdef"
skalberg@14516
   201
  "ROR_ONE_def" > "HOL4Word32.word32.ROR_ONE_def"
skalberg@14516
   202
  "ROR_ONE_WELLDEF" > "HOL4Word32.word32.ROR_ONE_WELLDEF"
skalberg@14516
   203
  "ROR_ONE_EVAL2" > "HOL4Word32.word32.ROR_ONE_EVAL2"
skalberg@14516
   204
  "ROR_ONE_EVAL" > "HOL4Word32.word32.ROR_ONE_EVAL"
skalberg@14516
   205
  "ROR_CYCLE" > "HOL4Word32.word32.ROR_CYCLE"
skalberg@14516
   206
  "ROR_ADD" > "HOL4Word32.word32.ROR_ADD"
skalberg@14516
   207
  "RIGHT_OR_OVER_ANDw" > "HOL4Word32.word32.RIGHT_OR_OVER_ANDw"
skalberg@14516
   208
  "RIGHT_OR_OVER_AND_QT" > "HOL4Word32.word32.RIGHT_OR_OVER_AND_QT"
skalberg@14516
   209
  "RIGHT_AND_OVER_ORw" > "HOL4Word32.word32.RIGHT_AND_OVER_ORw"
skalberg@14516
   210
  "RIGHT_AND_OVER_OR_QT" > "HOL4Word32.word32.RIGHT_AND_OVER_OR_QT"
skalberg@14516
   211
  "OR_primdef" > "HOL4Word32.word32.OR_primdef"
skalberg@14516
   212
  "OR_def" > "HOL4Word32.word32.OR_def"
skalberg@14516
   213
  "OR_IDEMw" > "HOL4Word32.word32.OR_IDEMw"
skalberg@14516
   214
  "OR_IDEM_QT" > "HOL4Word32.word32.OR_IDEM_QT"
skalberg@14516
   215
  "OR_EVAL2" > "HOL4Word32.word32.OR_EVAL2"
skalberg@14516
   216
  "OR_EVAL" > "HOL4Word32.word32.OR_EVAL"
skalberg@14516
   217
  "OR_COMP_QT" > "HOL4Word32.word32.OR_COMP_QT"
skalberg@14516
   218
  "OR_COMMw" > "HOL4Word32.word32.OR_COMMw"
skalberg@14516
   219
  "OR_COMM_QT" > "HOL4Word32.word32.OR_COMM_QT"
skalberg@14516
   220
  "OR_ASSOCw" > "HOL4Word32.word32.OR_ASSOCw"
skalberg@14516
   221
  "OR_ASSOC_QT" > "HOL4Word32.word32.OR_ASSOC_QT"
skalberg@14516
   222
  "OR_ABSORBw" > "HOL4Word32.word32.OR_ABSORBw"
skalberg@14516
   223
  "OR_ABSORB_QT" > "HOL4Word32.word32.OR_ABSORB_QT"
skalberg@14516
   224
  "ONE_COMPw" > "HOL4Word32.word32.ONE_COMPw"
skalberg@14516
   225
  "ONE_COMP_primdef" > "HOL4Word32.word32.ONE_COMP_primdef"
skalberg@14516
   226
  "ONE_COMP_def" > "HOL4Word32.word32.ONE_COMP_def"
skalberg@14516
   227
  "ONE_COMP_WELLDEF" > "HOL4Word32.word32.ONE_COMP_WELLDEF"
skalberg@14516
   228
  "ONE_COMP_TWO_COMP" > "HOL4Word32.word32.ONE_COMP_TWO_COMP"
skalberg@14516
   229
  "ONE_COMP_THM" > "HOL4Word32.word32.ONE_COMP_THM"
skalberg@14516
   230
  "ONE_COMP_QT" > "HOL4Word32.word32.ONE_COMP_QT"
skalberg@14516
   231
  "ONE_COMP_EVAL2" > "HOL4Word32.word32.ONE_COMP_EVAL2"
skalberg@14516
   232
  "ONE_COMP_EVAL" > "HOL4Word32.word32.ONE_COMP_EVAL"
skalberg@14516
   233
  "MUL_WELLDEF" > "HOL4Word32.word32.MUL_WELLDEF"
skalberg@14516
   234
  "MUL_EVAL2" > "HOL4Word32.word32.MUL_EVAL2"
skalberg@14516
   235
  "MUL_EVAL" > "HOL4Word32.word32.MUL_EVAL"
skalberg@14516
   236
  "MULT_QT" > "HOL4Word32.word32.MULT_QT"
skalberg@14516
   237
  "MULT_COMMw" > "HOL4Word32.word32.MULT_COMMw"
skalberg@14516
   238
  "MULT_COMM_QT" > "HOL4Word32.word32.MULT_COMM_QT"
skalberg@14516
   239
  "MULT_CLAUSESw" > "HOL4Word32.word32.MULT_CLAUSESw"
skalberg@14516
   240
  "MULT_CLAUSES_QT" > "HOL4Word32.word32.MULT_CLAUSES_QT"
skalberg@14516
   241
  "MULT_ASSOCw" > "HOL4Word32.word32.MULT_ASSOCw"
skalberg@14516
   242
  "MULT_ASSOC_QT" > "HOL4Word32.word32.MULT_ASSOC_QT"
skalberg@14516
   243
  "MSBn_primdef" > "HOL4Word32.word32.MSBn_primdef"
skalberg@14516
   244
  "MSBn_def" > "HOL4Word32.word32.MSBn_def"
skalberg@14516
   245
  "MSB_primdef" > "HOL4Word32.word32.MSB_primdef"
skalberg@14516
   246
  "MSB_def" > "HOL4Word32.word32.MSB_def"
skalberg@14516
   247
  "MSB_WELLDEF" > "HOL4Word32.word32.MSB_WELLDEF"
skalberg@14516
   248
  "MSB_EVAL2" > "HOL4Word32.word32.MSB_EVAL2"
skalberg@14516
   249
  "MSB_EVAL" > "HOL4Word32.word32.MSB_EVAL"
skalberg@14516
   250
  "MODw_primdef" > "HOL4Word32.word32.MODw_primdef"
skalberg@14516
   251
  "MODw_def" > "HOL4Word32.word32.MODw_def"
skalberg@14516
   252
  "MODw_THM" > "HOL4Word32.word32.MODw_THM"
skalberg@14516
   253
  "MODw_MULT" > "HOL4Word32.word32.MODw_MULT"
skalberg@14516
   254
  "MODw_IDEM2" > "HOL4Word32.word32.MODw_IDEM2"
skalberg@14516
   255
  "MODw_EVAL" > "HOL4Word32.word32.MODw_EVAL"
skalberg@14516
   256
  "MODw_ELIM" > "HOL4Word32.word32.MODw_ELIM"
skalberg@14516
   257
  "MOD_MOD_DIV_2EXP" > "HOL4Word32.word32.MOD_MOD_DIV_2EXP"
skalberg@14516
   258
  "MOD_MOD_DIV" > "HOL4Word32.word32.MOD_MOD_DIV"
skalberg@14516
   259
  "MOD_ADD" > "HOL4Word32.word32.MOD_ADD"
skalberg@14516
   260
  "LSR_THM" > "HOL4Word32.word32.LSR_THM"
skalberg@14516
   261
  "LSR_ONE_primdef" > "HOL4Word32.word32.LSR_ONE_primdef"
skalberg@14516
   262
  "LSR_ONE_def" > "HOL4Word32.word32.LSR_ONE_def"
skalberg@14516
   263
  "LSR_ONE_WELLDEF" > "HOL4Word32.word32.LSR_ONE_WELLDEF"
skalberg@14516
   264
  "LSR_ONE_EVAL2" > "HOL4Word32.word32.LSR_ONE_EVAL2"
skalberg@14516
   265
  "LSR_ONE_EVAL" > "HOL4Word32.word32.LSR_ONE_EVAL"
skalberg@14516
   266
  "LSR_ONE" > "HOL4Word32.word32.LSR_ONE"
skalberg@14516
   267
  "LSR_LIMIT" > "HOL4Word32.word32.LSR_LIMIT"
skalberg@14516
   268
  "LSR_EVAL" > "HOL4Word32.word32.LSR_EVAL"
skalberg@14516
   269
  "LSR_ADD" > "HOL4Word32.word32.LSR_ADD"
skalberg@14516
   270
  "LSL_LIMIT" > "HOL4Word32.word32.LSL_LIMIT"
skalberg@14516
   271
  "LSL_ADD" > "HOL4Word32.word32.LSL_ADD"
skalberg@14516
   272
  "LSB_primdef" > "HOL4Word32.word32.LSB_primdef"
skalberg@14516
   273
  "LSB_def" > "HOL4Word32.word32.LSB_def"
skalberg@14516
   274
  "LSB_WELLDEF" > "HOL4Word32.word32.LSB_WELLDEF"
skalberg@14516
   275
  "LSB_EVAL2" > "HOL4Word32.word32.LSB_EVAL2"
skalberg@14516
   276
  "LSB_EVAL" > "HOL4Word32.word32.LSB_EVAL"
skalberg@14516
   277
  "LEFT_SHIFT_LESS" > "HOL4Word32.word32.LEFT_SHIFT_LESS"
skalberg@14516
   278
  "LEFT_ADD_DISTRIBw" > "HOL4Word32.word32.LEFT_ADD_DISTRIBw"
skalberg@14516
   279
  "LEFT_ADD_DISTRIB_QT" > "HOL4Word32.word32.LEFT_ADD_DISTRIB_QT"
skalberg@14516
   280
  "INw_primdef" > "HOL4Word32.word32.INw_primdef"
skalberg@14516
   281
  "INw_def" > "HOL4Word32.word32.INw_def"
skalberg@14516
   282
  "INw_MODw" > "HOL4Word32.word32.INw_MODw"
skalberg@14516
   283
  "INV_SUC_EQ_QT" > "HOL4Word32.word32.INV_SUC_EQ_QT"
skalberg@14516
   284
  "HB_primdef" > "HOL4Word32.word32.HB_primdef"
skalberg@14516
   285
  "HB_def" > "HOL4Word32.word32.HB_def"
skalberg@14516
   286
  "FUNPOW_THM2" > "HOL4Word32.word32.FUNPOW_THM2"
skalberg@14516
   287
  "FUNPOW_THM" > "HOL4Word32.word32.FUNPOW_THM"
skalberg@14516
   288
  "FUNPOW_COMP" > "HOL4Word32.word32.FUNPOW_COMP"
skalberg@14516
   289
  "EQ_ADD_RCANCELw" > "HOL4Word32.word32.EQ_ADD_RCANCELw"
skalberg@14516
   290
  "EQ_ADD_RCANCEL_QT" > "HOL4Word32.word32.EQ_ADD_RCANCEL_QT"
skalberg@14516
   291
  "EQ_ADD_LCANCELw" > "HOL4Word32.word32.EQ_ADD_LCANCELw"
skalberg@14516
   292
  "EQ_ADD_LCANCEL_QT" > "HOL4Word32.word32.EQ_ADD_LCANCEL_QT"
skalberg@14516
   293
  "EQUIV_primdef" > "HOL4Word32.word32.EQUIV_primdef"
skalberg@14516
   294
  "EQUIV_def" > "HOL4Word32.word32.EQUIV_def"
skalberg@14516
   295
  "EQUIV_QT" > "HOL4Word32.word32.EQUIV_QT"
skalberg@14516
   296
  "EOR_primdef" > "HOL4Word32.word32.EOR_primdef"
skalberg@14516
   297
  "EOR_def" > "HOL4Word32.word32.EOR_def"
skalberg@14516
   298
  "EOR_EVAL2" > "HOL4Word32.word32.EOR_EVAL2"
skalberg@14516
   299
  "EOR_EVAL" > "HOL4Word32.word32.EOR_EVAL"
skalberg@14516
   300
  "DE_MORGAN_THMw" > "HOL4Word32.word32.DE_MORGAN_THMw"
skalberg@14516
   301
  "DE_MORGAN_THM_QT" > "HOL4Word32.word32.DE_MORGAN_THM_QT"
skalberg@14516
   302
  "COMP0_primdef" > "HOL4Word32.word32.COMP0_primdef"
skalberg@14516
   303
  "COMP0_def" > "HOL4Word32.word32.COMP0_def"
skalberg@14516
   304
  "CANCEL_SUBw" > "HOL4Word32.word32.CANCEL_SUBw"
skalberg@14516
   305
  "BITw_primdef" > "HOL4Word32.word32.BITw_primdef"
skalberg@14516
   306
  "BITw_def" > "HOL4Word32.word32.BITw_def"
skalberg@14516
   307
  "BITw_THM" > "HOL4Word32.word32.BITw_THM"
skalberg@14516
   308
  "BIT_EVAL" > "HOL4Word32.word32.BIT_EVAL"
skalberg@14516
   309
  "BIT_EQUIV_THM" > "HOL4Word32.word32.BIT_EQUIV_THM"
skalberg@14516
   310
  "BIT_EQUIV" > "HOL4Word32.word32.BIT_EQUIV"
skalberg@14516
   311
  "BITWISEw_WELLDEF" > "HOL4Word32.word32.BITWISEw_WELLDEF"
skalberg@14516
   312
  "BITWISE_WELLDEF" > "HOL4Word32.word32.BITWISE_WELLDEF"
skalberg@14516
   313
  "BITWISE_THM2" > "HOL4Word32.word32.BITWISE_THM2"
skalberg@14516
   314
  "BITWISE_ONE_COMP_THM" > "HOL4Word32.word32.BITWISE_ONE_COMP_THM"
skalberg@14516
   315
  "BITWISE_ISTEP" > "HOL4Word32.word32.BITWISE_ISTEP"
skalberg@14516
   316
  "BITWISE_EVAL2" > "HOL4Word32.word32.BITWISE_EVAL2"
skalberg@14516
   317
  "BITWISE_EVAL" > "HOL4Word32.word32.BITWISE_EVAL"
skalberg@14516
   318
  "BITSw_primdef" > "HOL4Word32.word32.BITSw_primdef"
skalberg@14516
   319
  "BITSw_def" > "HOL4Word32.word32.BITSw_def"
skalberg@14516
   320
  "BITSw_ZERO" > "HOL4Word32.word32.BITSw_ZERO"
skalberg@14516
   321
  "BITSw_DIV_THM" > "HOL4Word32.word32.BITSw_DIV_THM"
skalberg@14516
   322
  "BITSw_COMP_THM" > "HOL4Word32.word32.BITSw_COMP_THM"
skalberg@14516
   323
  "BITSwLT_THM" > "HOL4Word32.word32.BITSwLT_THM"
skalberg@14516
   324
  "BITS_SUC2" > "HOL4Word32.word32.BITS_SUC2"
skalberg@14516
   325
  "BITS_SLICEw_THM" > "HOL4Word32.word32.BITS_SLICEw_THM"
skalberg@14516
   326
  "BITS_EVAL" > "HOL4Word32.word32.BITS_EVAL"
skalberg@14516
   327
  "ASR_w_T" > "HOL4Word32.word32.ASR_w_T"
skalberg@14516
   328
  "ASR_THM" > "HOL4Word32.word32.ASR_THM"
skalberg@14516
   329
  "ASR_ONE_primdef" > "HOL4Word32.word32.ASR_ONE_primdef"
skalberg@14516
   330
  "ASR_ONE_def" > "HOL4Word32.word32.ASR_ONE_def"
skalberg@14516
   331
  "ASR_ONE_WELLDEF" > "HOL4Word32.word32.ASR_ONE_WELLDEF"
skalberg@14516
   332
  "ASR_ONE_EVAL2" > "HOL4Word32.word32.ASR_ONE_EVAL2"
skalberg@14516
   333
  "ASR_ONE_EVAL" > "HOL4Word32.word32.ASR_ONE_EVAL"
skalberg@14516
   334
  "ASR_LIMIT" > "HOL4Word32.word32.ASR_LIMIT"
skalberg@14516
   335
  "ASR_ADD" > "HOL4Word32.word32.ASR_ADD"
skalberg@14516
   336
  "AONE_primdef" > "HOL4Word32.word32.AONE_primdef"
skalberg@14516
   337
  "AONE_def" > "HOL4Word32.word32.AONE_def"
skalberg@14516
   338
  "AND_primdef" > "HOL4Word32.word32.AND_primdef"
skalberg@14516
   339
  "AND_def" > "HOL4Word32.word32.AND_def"
skalberg@14516
   340
  "AND_IDEMw" > "HOL4Word32.word32.AND_IDEMw"
skalberg@14516
   341
  "AND_IDEM_QT" > "HOL4Word32.word32.AND_IDEM_QT"
skalberg@14516
   342
  "AND_EVAL2" > "HOL4Word32.word32.AND_EVAL2"
skalberg@14516
   343
  "AND_EVAL" > "HOL4Word32.word32.AND_EVAL"
skalberg@14516
   344
  "AND_COMP_QT" > "HOL4Word32.word32.AND_COMP_QT"
skalberg@14516
   345
  "AND_COMMw" > "HOL4Word32.word32.AND_COMMw"
skalberg@14516
   346
  "AND_COMM_QT" > "HOL4Word32.word32.AND_COMM_QT"
skalberg@14516
   347
  "AND_ASSOCw" > "HOL4Word32.word32.AND_ASSOCw"
skalberg@14516
   348
  "AND_ASSOC_QT" > "HOL4Word32.word32.AND_ASSOC_QT"
skalberg@14516
   349
  "AND_ABSORBw" > "HOL4Word32.word32.AND_ABSORBw"
skalberg@14516
   350
  "AND_ABSORB_QT" > "HOL4Word32.word32.AND_ABSORB_QT"
skalberg@14516
   351
  "ADDw" > "HOL4Word32.word32.ADDw"
skalberg@14516
   352
  "ADD_WELLDEF" > "HOL4Word32.word32.ADD_WELLDEF"
skalberg@14516
   353
  "ADD_TWO_COMP_QT" > "HOL4Word32.word32.ADD_TWO_COMP_QT"
skalberg@14516
   354
  "ADD_TWO_COMP2" > "HOL4Word32.word32.ADD_TWO_COMP2"
skalberg@14516
   355
  "ADD_TWO_COMP" > "HOL4Word32.word32.ADD_TWO_COMP"
skalberg@14516
   356
  "ADD_SUBw" > "HOL4Word32.word32.ADD_SUBw"
skalberg@14516
   357
  "ADD_SUB_SYM" > "HOL4Word32.word32.ADD_SUB_SYM"
skalberg@14516
   358
  "ADD_SUB_ASSOC" > "HOL4Word32.word32.ADD_SUB_ASSOC"
skalberg@14516
   359
  "ADD_QT" > "HOL4Word32.word32.ADD_QT"
skalberg@14516
   360
  "ADD_INV_0_QT" > "HOL4Word32.word32.ADD_INV_0_QT"
skalberg@14516
   361
  "ADD_INV_0_EQw" > "HOL4Word32.word32.ADD_INV_0_EQw"
skalberg@14516
   362
  "ADD_INV_0_EQ_QT" > "HOL4Word32.word32.ADD_INV_0_EQ_QT"
skalberg@14516
   363
  "ADD_EVAL2" > "HOL4Word32.word32.ADD_EVAL2"
skalberg@14516
   364
  "ADD_EVAL" > "HOL4Word32.word32.ADD_EVAL"
skalberg@14516
   365
  "ADD_EQ_SUBw" > "HOL4Word32.word32.ADD_EQ_SUBw"
skalberg@14516
   366
  "ADD_COMMw" > "HOL4Word32.word32.ADD_COMMw"
skalberg@14516
   367
  "ADD_COMM_QT" > "HOL4Word32.word32.ADD_COMM_QT"
skalberg@14516
   368
  "ADD_CLAUSESw" > "HOL4Word32.word32.ADD_CLAUSESw"
skalberg@14516
   369
  "ADD_CLAUSES_QT" > "HOL4Word32.word32.ADD_CLAUSES_QT"
skalberg@14516
   370
  "ADD_ASSOCw" > "HOL4Word32.word32.ADD_ASSOCw"
skalberg@14516
   371
  "ADD_ASSOC_QT" > "HOL4Word32.word32.ADD_ASSOC_QT"
skalberg@14516
   372
  "ADD_0w" > "HOL4Word32.word32.ADD_0w"
skalberg@14516
   373
  "ADD_0_QT" > "HOL4Word32.word32.ADD_0_QT"
skalberg@14516
   374
  "ADD1w" > "HOL4Word32.word32.ADD1w"
skalberg@14516
   375
  "ADD1_QT" > "HOL4Word32.word32.ADD1_QT"
skalberg@14516
   376
skalberg@14516
   377
end