src/HOL/Import/HOL/word32.imp
changeset 14516 a183dec876ab
child 44763 b50d5d694838
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL/word32.imp	Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,377 @@
+import
+
+import_segment "hol4"
+
+def_maps
+  "word_suc" > "word_suc_def"
+  "word_sub" > "word_sub_def"
+  "word_ror1" > "word_ror1_def"
+  "word_ror" > "word_ror_def"
+  "word_mul" > "word_mul_def"
+  "word_lsr1" > "word_lsr1_def"
+  "word_lsr" > "word_lsr_def"
+  "word_lsl" > "word_lsl_def"
+  "word_asr1" > "word_asr1_def"
+  "word_asr" > "word_asr_def"
+  "word_add" > "word_add_def"
+  "word_2comp" > "word_2comp_def"
+  "word_1comp" > "word_1comp_def"
+  "w_T" > "w_T_primdef"
+  "w_1" > "w_1_primdef"
+  "w_0" > "w_0_primdef"
+  "w2n" > "w2n_primdef"
+  "n2w" > "n2w_primdef"
+  "mk_word32" > "mk_word32_def"
+  "dest_word32" > "dest_word32_def"
+  "bitwise_or" > "bitwise_or_def"
+  "bitwise_eor" > "bitwise_eor_def"
+  "bitwise_and" > "bitwise_and_def"
+  "WL" > "WL_primdef"
+  "TWO_COMP" > "TWO_COMP_primdef"
+  "TOw" > "TOw_primdef"
+  "SLICEw" > "SLICEw_primdef"
+  "RRXn" > "RRXn_primdef"
+  "RRX" > "RRX_primdef"
+  "ROR_ONE" > "ROR_ONE_primdef"
+  "OR" > "OR_primdef"
+  "ONE_COMP" > "ONE_COMP_primdef"
+  "MSBn" > "MSBn_primdef"
+  "MSB" > "MSB_primdef"
+  "MODw" > "MODw_primdef"
+  "LSR_ONE" > "LSR_ONE_primdef"
+  "LSB" > "LSB_primdef"
+  "INw" > "INw_primdef"
+  "HB" > "HB_primdef"
+  "EQUIV" > "EQUIV_primdef"
+  "EOR" > "EOR_primdef"
+  "COMP0" > "COMP0_primdef"
+  "BITw" > "BITw_primdef"
+  "BITSw" > "BITSw_primdef"
+  "ASR_ONE" > "ASR_ONE_primdef"
+  "AONE" > "AONE_primdef"
+  "AND" > "AND_primdef"
+
+type_maps
+  "word32" > "HOL4Word32.word32.word32"
+
+const_maps
+  "word_suc" > "HOL4Word32.word32.word_suc"
+  "word_sub" > "HOL4Word32.word32.word_sub"
+  "word_ror1" > "HOL4Word32.word32.word_ror1"
+  "word_ror" > "HOL4Word32.word32.word_ror"
+  "word_mul" > "HOL4Word32.word32.word_mul"
+  "word_lsr1" > "HOL4Word32.word32.word_lsr1"
+  "word_lsr" > "HOL4Word32.word32.word_lsr"
+  "word_lsl" > "HOL4Word32.word32.word_lsl"
+  "word_asr1" > "HOL4Word32.word32.word_asr1"
+  "word_asr" > "HOL4Word32.word32.word_asr"
+  "word_add" > "HOL4Word32.word32.word_add"
+  "word_2comp" > "HOL4Word32.word32.word_2comp"
+  "word_1comp" > "HOL4Word32.word32.word_1comp"
+  "w_T" > "HOL4Word32.word32.w_T"
+  "w_1" > "HOL4Word32.word32.w_1"
+  "w_0" > "HOL4Word32.word32.w_0"
+  "w2n" > "HOL4Word32.word32.w2n"
+  "n2w" > "HOL4Word32.word32.n2w"
+  "bitwise_or" > "HOL4Word32.word32.bitwise_or"
+  "bitwise_eor" > "HOL4Word32.word32.bitwise_eor"
+  "bitwise_and" > "HOL4Word32.word32.bitwise_and"
+  "WL" > "HOL4Word32.word32.WL"
+  "TWO_COMP" > "HOL4Word32.word32.TWO_COMP"
+  "TOw" > "HOL4Word32.word32.TOw"
+  "SLICEw" > "HOL4Word32.word32.SLICEw"
+  "RRXn" > "HOL4Word32.word32.RRXn"
+  "RRX" > "HOL4Word32.word32.RRX"
+  "ROR_ONE" > "HOL4Word32.word32.ROR_ONE"
+  "OR" > "HOL4Word32.word32.OR"
+  "ONE_COMP" > "HOL4Word32.word32.ONE_COMP"
+  "MSBn" > "HOL4Word32.word32.MSBn"
+  "MSB" > "HOL4Word32.word32.MSB"
+  "MODw" > "HOL4Word32.word32.MODw"
+  "LSR_ONE" > "HOL4Word32.word32.LSR_ONE"
+  "LSB" > "HOL4Word32.word32.LSB"
+  "INw" > "HOL4Word32.word32.INw"
+  "HB" > "HOL4Word32.word32.HB"
+  "EQUIV" > "HOL4Word32.word32.EQUIV"
+  "EOR" > "HOL4Word32.word32.EOR"
+  "COMP0" > "HOL4Word32.word32.COMP0"
+  "BITw" > "HOL4Word32.word32.BITw"
+  "BITSw" > "HOL4Word32.word32.BITSw"
+  "ASR_ONE" > "HOL4Word32.word32.ASR_ONE"
+  "AONE" > "HOL4Word32.word32.AONE"
+  "AND" > "HOL4Word32.word32.AND"
+
+const_renames
+  "==" > "EQUIV"
+
+thm_maps
+  "word_suc_def" > "HOL4Word32.word32.word_suc_def"
+  "word_suc" > "HOL4Word32.word32.word_suc"
+  "word_sub_def" > "HOL4Word32.word32.word_sub_def"
+  "word_sub" > "HOL4Word32.word32.word_sub"
+  "word_ror_def" > "HOL4Word32.word32.word_ror_def"
+  "word_ror1_def" > "HOL4Word32.word32.word_ror1_def"
+  "word_ror1" > "HOL4Word32.word32.word_ror1"
+  "word_ror" > "HOL4Word32.word32.word_ror"
+  "word_nchotomy" > "HOL4Word32.word32.word_nchotomy"
+  "word_mul_def" > "HOL4Word32.word32.word_mul_def"
+  "word_mul" > "HOL4Word32.word32.word_mul"
+  "word_lsr_def" > "HOL4Word32.word32.word_lsr_def"
+  "word_lsr1_def" > "HOL4Word32.word32.word_lsr1_def"
+  "word_lsr1" > "HOL4Word32.word32.word_lsr1"
+  "word_lsr" > "HOL4Word32.word32.word_lsr"
+  "word_lsl_def" > "HOL4Word32.word32.word_lsl_def"
+  "word_lsl" > "HOL4Word32.word32.word_lsl"
+  "word_asr_def" > "HOL4Word32.word32.word_asr_def"
+  "word_asr1_def" > "HOL4Word32.word32.word_asr1_def"
+  "word_asr1" > "HOL4Word32.word32.word_asr1"
+  "word_asr" > "HOL4Word32.word32.word_asr"
+  "word_add_def" > "HOL4Word32.word32.word_add_def"
+  "word_add" > "HOL4Word32.word32.word_add"
+  "word_2comp_def" > "HOL4Word32.word32.word_2comp_def"
+  "word_2comp" > "HOL4Word32.word32.word_2comp"
+  "word_1comp_def" > "HOL4Word32.word32.word_1comp_def"
+  "word_1comp" > "HOL4Word32.word32.word_1comp"
+  "word32_tybij" > "HOL4Word32.word32.word32_tybij"
+  "word32_TY_DEF" > "HOL4Word32.word32.word32_TY_DEF"
+  "w_T_primdef" > "HOL4Word32.word32.w_T_primdef"
+  "w_T_def" > "HOL4Word32.word32.w_T_def"
+  "w_T" > "HOL4Word32.word32.w_T"
+  "w_1_primdef" > "HOL4Word32.word32.w_1_primdef"
+  "w_1_def" > "HOL4Word32.word32.w_1_def"
+  "w_1" > "HOL4Word32.word32.w_1"
+  "w_0_primdef" > "HOL4Word32.word32.w_0_primdef"
+  "w_0_def" > "HOL4Word32.word32.w_0_def"
+  "w_0" > "HOL4Word32.word32.w_0"
+  "w2n_primdef" > "HOL4Word32.word32.w2n_primdef"
+  "w2n_def" > "HOL4Word32.word32.w2n_def"
+  "w2n_EVAL" > "HOL4Word32.word32.w2n_EVAL"
+  "w2n_ELIM" > "HOL4Word32.word32.w2n_ELIM"
+  "n2w_primdef" > "HOL4Word32.word32.n2w_primdef"
+  "n2w_def" > "HOL4Word32.word32.n2w_def"
+  "n2w_11" > "HOL4Word32.word32.n2w_11"
+  "dest_word_mk_word_eq3" > "HOL4Word32.word32.dest_word_mk_word_eq3"
+  "bitwise_or_def" > "HOL4Word32.word32.bitwise_or_def"
+  "bitwise_or" > "HOL4Word32.word32.bitwise_or"
+  "bitwise_eor_def" > "HOL4Word32.word32.bitwise_eor_def"
+  "bitwise_eor" > "HOL4Word32.word32.bitwise_eor"
+  "bitwise_and_def" > "HOL4Word32.word32.bitwise_and_def"
+  "bitwise_and" > "HOL4Word32.word32.bitwise_and"
+  "ZERO_SHIFT2" > "HOL4Word32.word32.ZERO_SHIFT2"
+  "ZERO_SHIFT" > "HOL4Word32.word32.ZERO_SHIFT"
+  "WL_primdef" > "HOL4Word32.word32.WL_primdef"
+  "WL_def" > "HOL4Word32.word32.WL_def"
+  "TWO_COMP_primdef" > "HOL4Word32.word32.TWO_COMP_primdef"
+  "TWO_COMP_def" > "HOL4Word32.word32.TWO_COMP_def"
+  "TWO_COMP_WELLDEF" > "HOL4Word32.word32.TWO_COMP_WELLDEF"
+  "TWO_COMP_ONE_COMP_QT" > "HOL4Word32.word32.TWO_COMP_ONE_COMP_QT"
+  "TWO_COMP_ONE_COMP" > "HOL4Word32.word32.TWO_COMP_ONE_COMP"
+  "TWO_COMP_EVAL2" > "HOL4Word32.word32.TWO_COMP_EVAL2"
+  "TWO_COMP_EVAL" > "HOL4Word32.word32.TWO_COMP_EVAL"
+  "TWO_COMP_ELIM" > "HOL4Word32.word32.TWO_COMP_ELIM"
+  "TWO_COMP_ADD" > "HOL4Word32.word32.TWO_COMP_ADD"
+  "TOw_primdef" > "HOL4Word32.word32.TOw_primdef"
+  "TOw_def" > "HOL4Word32.word32.TOw_def"
+  "TOw_WELLDEF" > "HOL4Word32.word32.TOw_WELLDEF"
+  "TOw_QT" > "HOL4Word32.word32.TOw_QT"
+  "TOw_IDEM" > "HOL4Word32.word32.TOw_IDEM"
+  "SUC_WELLDEF" > "HOL4Word32.word32.SUC_WELLDEF"
+  "SUC_EQUIV_COMP" > "HOL4Word32.word32.SUC_EQUIV_COMP"
+  "SUBw" > "HOL4Word32.word32.SUBw"
+  "SUB_SUBw" > "HOL4Word32.word32.SUB_SUBw"
+  "SUB_PLUSw" > "HOL4Word32.word32.SUB_PLUSw"
+  "SUB_EQUALw" > "HOL4Word32.word32.SUB_EQUALw"
+  "SLICEw_primdef" > "HOL4Word32.word32.SLICEw_primdef"
+  "SLICEw_def" > "HOL4Word32.word32.SLICEw_def"
+  "SLICEw_ZERO_THM" > "HOL4Word32.word32.SLICEw_ZERO_THM"
+  "SLICEw_ZERO" > "HOL4Word32.word32.SLICEw_ZERO"
+  "SLICEw_THM" > "HOL4Word32.word32.SLICEw_THM"
+  "SLICEw_COMP_THM" > "HOL4Word32.word32.SLICEw_COMP_THM"
+  "SLICE_EVAL" > "HOL4Word32.word32.SLICE_EVAL"
+  "RRXn_primdef" > "HOL4Word32.word32.RRXn_primdef"
+  "RRXn_def" > "HOL4Word32.word32.RRXn_def"
+  "RRX_primdef" > "HOL4Word32.word32.RRX_primdef"
+  "RRX_def" > "HOL4Word32.word32.RRX_def"
+  "RRX_WELLDEF" > "HOL4Word32.word32.RRX_WELLDEF"
+  "RRX_EVAL2" > "HOL4Word32.word32.RRX_EVAL2"
+  "RRX_EVAL" > "HOL4Word32.word32.RRX_EVAL"
+  "ROR_w_T" > "HOL4Word32.word32.ROR_w_T"
+  "ROR_THM" > "HOL4Word32.word32.ROR_THM"
+  "ROR_ONE_primdef" > "HOL4Word32.word32.ROR_ONE_primdef"
+  "ROR_ONE_def" > "HOL4Word32.word32.ROR_ONE_def"
+  "ROR_ONE_WELLDEF" > "HOL4Word32.word32.ROR_ONE_WELLDEF"
+  "ROR_ONE_EVAL2" > "HOL4Word32.word32.ROR_ONE_EVAL2"
+  "ROR_ONE_EVAL" > "HOL4Word32.word32.ROR_ONE_EVAL"
+  "ROR_CYCLE" > "HOL4Word32.word32.ROR_CYCLE"
+  "ROR_ADD" > "HOL4Word32.word32.ROR_ADD"
+  "RIGHT_OR_OVER_ANDw" > "HOL4Word32.word32.RIGHT_OR_OVER_ANDw"
+  "RIGHT_OR_OVER_AND_QT" > "HOL4Word32.word32.RIGHT_OR_OVER_AND_QT"
+  "RIGHT_AND_OVER_ORw" > "HOL4Word32.word32.RIGHT_AND_OVER_ORw"
+  "RIGHT_AND_OVER_OR_QT" > "HOL4Word32.word32.RIGHT_AND_OVER_OR_QT"
+  "OR_primdef" > "HOL4Word32.word32.OR_primdef"
+  "OR_def" > "HOL4Word32.word32.OR_def"
+  "OR_IDEMw" > "HOL4Word32.word32.OR_IDEMw"
+  "OR_IDEM_QT" > "HOL4Word32.word32.OR_IDEM_QT"
+  "OR_EVAL2" > "HOL4Word32.word32.OR_EVAL2"
+  "OR_EVAL" > "HOL4Word32.word32.OR_EVAL"
+  "OR_COMP_QT" > "HOL4Word32.word32.OR_COMP_QT"
+  "OR_COMMw" > "HOL4Word32.word32.OR_COMMw"
+  "OR_COMM_QT" > "HOL4Word32.word32.OR_COMM_QT"
+  "OR_ASSOCw" > "HOL4Word32.word32.OR_ASSOCw"
+  "OR_ASSOC_QT" > "HOL4Word32.word32.OR_ASSOC_QT"
+  "OR_ABSORBw" > "HOL4Word32.word32.OR_ABSORBw"
+  "OR_ABSORB_QT" > "HOL4Word32.word32.OR_ABSORB_QT"
+  "ONE_COMPw" > "HOL4Word32.word32.ONE_COMPw"
+  "ONE_COMP_primdef" > "HOL4Word32.word32.ONE_COMP_primdef"
+  "ONE_COMP_def" > "HOL4Word32.word32.ONE_COMP_def"
+  "ONE_COMP_WELLDEF" > "HOL4Word32.word32.ONE_COMP_WELLDEF"
+  "ONE_COMP_TWO_COMP" > "HOL4Word32.word32.ONE_COMP_TWO_COMP"
+  "ONE_COMP_THM" > "HOL4Word32.word32.ONE_COMP_THM"
+  "ONE_COMP_QT" > "HOL4Word32.word32.ONE_COMP_QT"
+  "ONE_COMP_EVAL2" > "HOL4Word32.word32.ONE_COMP_EVAL2"
+  "ONE_COMP_EVAL" > "HOL4Word32.word32.ONE_COMP_EVAL"
+  "MUL_WELLDEF" > "HOL4Word32.word32.MUL_WELLDEF"
+  "MUL_EVAL2" > "HOL4Word32.word32.MUL_EVAL2"
+  "MUL_EVAL" > "HOL4Word32.word32.MUL_EVAL"
+  "MULT_QT" > "HOL4Word32.word32.MULT_QT"
+  "MULT_COMMw" > "HOL4Word32.word32.MULT_COMMw"
+  "MULT_COMM_QT" > "HOL4Word32.word32.MULT_COMM_QT"
+  "MULT_CLAUSESw" > "HOL4Word32.word32.MULT_CLAUSESw"
+  "MULT_CLAUSES_QT" > "HOL4Word32.word32.MULT_CLAUSES_QT"
+  "MULT_ASSOCw" > "HOL4Word32.word32.MULT_ASSOCw"
+  "MULT_ASSOC_QT" > "HOL4Word32.word32.MULT_ASSOC_QT"
+  "MSBn_primdef" > "HOL4Word32.word32.MSBn_primdef"
+  "MSBn_def" > "HOL4Word32.word32.MSBn_def"
+  "MSB_primdef" > "HOL4Word32.word32.MSB_primdef"
+  "MSB_def" > "HOL4Word32.word32.MSB_def"
+  "MSB_WELLDEF" > "HOL4Word32.word32.MSB_WELLDEF"
+  "MSB_EVAL2" > "HOL4Word32.word32.MSB_EVAL2"
+  "MSB_EVAL" > "HOL4Word32.word32.MSB_EVAL"
+  "MODw_primdef" > "HOL4Word32.word32.MODw_primdef"
+  "MODw_def" > "HOL4Word32.word32.MODw_def"
+  "MODw_THM" > "HOL4Word32.word32.MODw_THM"
+  "MODw_MULT" > "HOL4Word32.word32.MODw_MULT"
+  "MODw_IDEM2" > "HOL4Word32.word32.MODw_IDEM2"
+  "MODw_EVAL" > "HOL4Word32.word32.MODw_EVAL"
+  "MODw_ELIM" > "HOL4Word32.word32.MODw_ELIM"
+  "MOD_MOD_DIV_2EXP" > "HOL4Word32.word32.MOD_MOD_DIV_2EXP"
+  "MOD_MOD_DIV" > "HOL4Word32.word32.MOD_MOD_DIV"
+  "MOD_ADD" > "HOL4Word32.word32.MOD_ADD"
+  "LSR_THM" > "HOL4Word32.word32.LSR_THM"
+  "LSR_ONE_primdef" > "HOL4Word32.word32.LSR_ONE_primdef"
+  "LSR_ONE_def" > "HOL4Word32.word32.LSR_ONE_def"
+  "LSR_ONE_WELLDEF" > "HOL4Word32.word32.LSR_ONE_WELLDEF"
+  "LSR_ONE_EVAL2" > "HOL4Word32.word32.LSR_ONE_EVAL2"
+  "LSR_ONE_EVAL" > "HOL4Word32.word32.LSR_ONE_EVAL"
+  "LSR_ONE" > "HOL4Word32.word32.LSR_ONE"
+  "LSR_LIMIT" > "HOL4Word32.word32.LSR_LIMIT"
+  "LSR_EVAL" > "HOL4Word32.word32.LSR_EVAL"
+  "LSR_ADD" > "HOL4Word32.word32.LSR_ADD"
+  "LSL_LIMIT" > "HOL4Word32.word32.LSL_LIMIT"
+  "LSL_ADD" > "HOL4Word32.word32.LSL_ADD"
+  "LSB_primdef" > "HOL4Word32.word32.LSB_primdef"
+  "LSB_def" > "HOL4Word32.word32.LSB_def"
+  "LSB_WELLDEF" > "HOL4Word32.word32.LSB_WELLDEF"
+  "LSB_EVAL2" > "HOL4Word32.word32.LSB_EVAL2"
+  "LSB_EVAL" > "HOL4Word32.word32.LSB_EVAL"
+  "LEFT_SHIFT_LESS" > "HOL4Word32.word32.LEFT_SHIFT_LESS"
+  "LEFT_ADD_DISTRIBw" > "HOL4Word32.word32.LEFT_ADD_DISTRIBw"
+  "LEFT_ADD_DISTRIB_QT" > "HOL4Word32.word32.LEFT_ADD_DISTRIB_QT"
+  "INw_primdef" > "HOL4Word32.word32.INw_primdef"
+  "INw_def" > "HOL4Word32.word32.INw_def"
+  "INw_MODw" > "HOL4Word32.word32.INw_MODw"
+  "INV_SUC_EQ_QT" > "HOL4Word32.word32.INV_SUC_EQ_QT"
+  "HB_primdef" > "HOL4Word32.word32.HB_primdef"
+  "HB_def" > "HOL4Word32.word32.HB_def"
+  "FUNPOW_THM2" > "HOL4Word32.word32.FUNPOW_THM2"
+  "FUNPOW_THM" > "HOL4Word32.word32.FUNPOW_THM"
+  "FUNPOW_COMP" > "HOL4Word32.word32.FUNPOW_COMP"
+  "EQ_ADD_RCANCELw" > "HOL4Word32.word32.EQ_ADD_RCANCELw"
+  "EQ_ADD_RCANCEL_QT" > "HOL4Word32.word32.EQ_ADD_RCANCEL_QT"
+  "EQ_ADD_LCANCELw" > "HOL4Word32.word32.EQ_ADD_LCANCELw"
+  "EQ_ADD_LCANCEL_QT" > "HOL4Word32.word32.EQ_ADD_LCANCEL_QT"
+  "EQUIV_primdef" > "HOL4Word32.word32.EQUIV_primdef"
+  "EQUIV_def" > "HOL4Word32.word32.EQUIV_def"
+  "EQUIV_QT" > "HOL4Word32.word32.EQUIV_QT"
+  "EOR_primdef" > "HOL4Word32.word32.EOR_primdef"
+  "EOR_def" > "HOL4Word32.word32.EOR_def"
+  "EOR_EVAL2" > "HOL4Word32.word32.EOR_EVAL2"
+  "EOR_EVAL" > "HOL4Word32.word32.EOR_EVAL"
+  "DE_MORGAN_THMw" > "HOL4Word32.word32.DE_MORGAN_THMw"
+  "DE_MORGAN_THM_QT" > "HOL4Word32.word32.DE_MORGAN_THM_QT"
+  "COMP0_primdef" > "HOL4Word32.word32.COMP0_primdef"
+  "COMP0_def" > "HOL4Word32.word32.COMP0_def"
+  "CANCEL_SUBw" > "HOL4Word32.word32.CANCEL_SUBw"
+  "BITw_primdef" > "HOL4Word32.word32.BITw_primdef"
+  "BITw_def" > "HOL4Word32.word32.BITw_def"
+  "BITw_THM" > "HOL4Word32.word32.BITw_THM"
+  "BIT_EVAL" > "HOL4Word32.word32.BIT_EVAL"
+  "BIT_EQUIV_THM" > "HOL4Word32.word32.BIT_EQUIV_THM"
+  "BIT_EQUIV" > "HOL4Word32.word32.BIT_EQUIV"
+  "BITWISEw_WELLDEF" > "HOL4Word32.word32.BITWISEw_WELLDEF"
+  "BITWISE_WELLDEF" > "HOL4Word32.word32.BITWISE_WELLDEF"
+  "BITWISE_THM2" > "HOL4Word32.word32.BITWISE_THM2"
+  "BITWISE_ONE_COMP_THM" > "HOL4Word32.word32.BITWISE_ONE_COMP_THM"
+  "BITWISE_ISTEP" > "HOL4Word32.word32.BITWISE_ISTEP"
+  "BITWISE_EVAL2" > "HOL4Word32.word32.BITWISE_EVAL2"
+  "BITWISE_EVAL" > "HOL4Word32.word32.BITWISE_EVAL"
+  "BITSw_primdef" > "HOL4Word32.word32.BITSw_primdef"
+  "BITSw_def" > "HOL4Word32.word32.BITSw_def"
+  "BITSw_ZERO" > "HOL4Word32.word32.BITSw_ZERO"
+  "BITSw_DIV_THM" > "HOL4Word32.word32.BITSw_DIV_THM"
+  "BITSw_COMP_THM" > "HOL4Word32.word32.BITSw_COMP_THM"
+  "BITSwLT_THM" > "HOL4Word32.word32.BITSwLT_THM"
+  "BITS_SUC2" > "HOL4Word32.word32.BITS_SUC2"
+  "BITS_SLICEw_THM" > "HOL4Word32.word32.BITS_SLICEw_THM"
+  "BITS_EVAL" > "HOL4Word32.word32.BITS_EVAL"
+  "ASR_w_T" > "HOL4Word32.word32.ASR_w_T"
+  "ASR_THM" > "HOL4Word32.word32.ASR_THM"
+  "ASR_ONE_primdef" > "HOL4Word32.word32.ASR_ONE_primdef"
+  "ASR_ONE_def" > "HOL4Word32.word32.ASR_ONE_def"
+  "ASR_ONE_WELLDEF" > "HOL4Word32.word32.ASR_ONE_WELLDEF"
+  "ASR_ONE_EVAL2" > "HOL4Word32.word32.ASR_ONE_EVAL2"
+  "ASR_ONE_EVAL" > "HOL4Word32.word32.ASR_ONE_EVAL"
+  "ASR_LIMIT" > "HOL4Word32.word32.ASR_LIMIT"
+  "ASR_ADD" > "HOL4Word32.word32.ASR_ADD"
+  "AONE_primdef" > "HOL4Word32.word32.AONE_primdef"
+  "AONE_def" > "HOL4Word32.word32.AONE_def"
+  "AND_primdef" > "HOL4Word32.word32.AND_primdef"
+  "AND_def" > "HOL4Word32.word32.AND_def"
+  "AND_IDEMw" > "HOL4Word32.word32.AND_IDEMw"
+  "AND_IDEM_QT" > "HOL4Word32.word32.AND_IDEM_QT"
+  "AND_EVAL2" > "HOL4Word32.word32.AND_EVAL2"
+  "AND_EVAL" > "HOL4Word32.word32.AND_EVAL"
+  "AND_COMP_QT" > "HOL4Word32.word32.AND_COMP_QT"
+  "AND_COMMw" > "HOL4Word32.word32.AND_COMMw"
+  "AND_COMM_QT" > "HOL4Word32.word32.AND_COMM_QT"
+  "AND_ASSOCw" > "HOL4Word32.word32.AND_ASSOCw"
+  "AND_ASSOC_QT" > "HOL4Word32.word32.AND_ASSOC_QT"
+  "AND_ABSORBw" > "HOL4Word32.word32.AND_ABSORBw"
+  "AND_ABSORB_QT" > "HOL4Word32.word32.AND_ABSORB_QT"
+  "ADDw" > "HOL4Word32.word32.ADDw"
+  "ADD_WELLDEF" > "HOL4Word32.word32.ADD_WELLDEF"
+  "ADD_TWO_COMP_QT" > "HOL4Word32.word32.ADD_TWO_COMP_QT"
+  "ADD_TWO_COMP2" > "HOL4Word32.word32.ADD_TWO_COMP2"
+  "ADD_TWO_COMP" > "HOL4Word32.word32.ADD_TWO_COMP"
+  "ADD_SUBw" > "HOL4Word32.word32.ADD_SUBw"
+  "ADD_SUB_SYM" > "HOL4Word32.word32.ADD_SUB_SYM"
+  "ADD_SUB_ASSOC" > "HOL4Word32.word32.ADD_SUB_ASSOC"
+  "ADD_QT" > "HOL4Word32.word32.ADD_QT"
+  "ADD_INV_0_QT" > "HOL4Word32.word32.ADD_INV_0_QT"
+  "ADD_INV_0_EQw" > "HOL4Word32.word32.ADD_INV_0_EQw"
+  "ADD_INV_0_EQ_QT" > "HOL4Word32.word32.ADD_INV_0_EQ_QT"
+  "ADD_EVAL2" > "HOL4Word32.word32.ADD_EVAL2"
+  "ADD_EVAL" > "HOL4Word32.word32.ADD_EVAL"
+  "ADD_EQ_SUBw" > "HOL4Word32.word32.ADD_EQ_SUBw"
+  "ADD_COMMw" > "HOL4Word32.word32.ADD_COMMw"
+  "ADD_COMM_QT" > "HOL4Word32.word32.ADD_COMM_QT"
+  "ADD_CLAUSESw" > "HOL4Word32.word32.ADD_CLAUSESw"
+  "ADD_CLAUSES_QT" > "HOL4Word32.word32.ADD_CLAUSES_QT"
+  "ADD_ASSOCw" > "HOL4Word32.word32.ADD_ASSOCw"
+  "ADD_ASSOC_QT" > "HOL4Word32.word32.ADD_ASSOC_QT"
+  "ADD_0w" > "HOL4Word32.word32.ADD_0w"
+  "ADD_0_QT" > "HOL4Word32.word32.ADD_0_QT"
+  "ADD1w" > "HOL4Word32.word32.ADD1w"
+  "ADD1_QT" > "HOL4Word32.word32.ADD1_QT"
+
+end