equal
deleted
inserted
replaced
|
1 import |
|
2 |
|
3 import_segment "hol4" |
|
4 |
|
5 def_maps |
|
6 "ICARRY" > "ICARRY_def" |
|
7 "ACARRY" > "ACARRY_def" |
|
8 |
|
9 thm_maps |
|
10 "WSEG_NBWORD_ADD" > "HOL4Vec.bword_arith.WSEG_NBWORD_ADD" |
|
11 "ICARRY_WSEG" > "HOL4Vec.bword_arith.ICARRY_WSEG" |
|
12 "ICARRY_DEF" > "HOL4Vec.bword_arith.ICARRY_DEF" |
|
13 "BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.BNVAL_LESS_EQ" |
|
14 "ADD_WORD_SPLIT" > "HOL4Vec.bword_arith.ADD_WORD_SPLIT" |
|
15 "ADD_NBWORD_EQ0_SPLIT" > "HOL4Vec.bword_arith.ADD_NBWORD_EQ0_SPLIT" |
|
16 "ADD_BV_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ1" |
|
17 "ADD_BV_BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ" |
|
18 "ADD_BV_BNVAL_DIV_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_DIV_LESS_EQ1" |
|
19 "ADD_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BNVAL_LESS_EQ1" |
|
20 "ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_WSEG" |
|
21 "ACARRY_MSB" > "HOL4Vec.bword_arith.ACARRY_MSB" |
|
22 "ACARRY_EQ_ICARRY" > "HOL4Vec.bword_arith.ACARRY_EQ_ICARRY" |
|
23 "ACARRY_EQ_ADD_DIV" > "HOL4Vec.bword_arith.ACARRY_EQ_ADD_DIV" |
|
24 "ACARRY_DEF" > "HOL4Vec.bword_arith.ACARRY_DEF" |
|
25 "ACARRY_ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_ACARRY_WSEG" |
|
26 |
|
27 end |