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