|
14516
|
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
|