|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"WXOR" > "WXOR_def"
|
|
|
7 |
"WOR" > "WOR_def"
|
|
|
8 |
"WNOT" > "WNOT_def"
|
|
|
9 |
"WAND" > "WAND_def"
|
|
|
10 |
|
|
|
11 |
thm_maps
|
|
|
12 |
"WXOR_DEF" > "HOL4Vec.bword_bitop.WXOR_DEF"
|
|
|
13 |
"WOR_DEF" > "HOL4Vec.bword_bitop.WOR_DEF"
|
|
|
14 |
"WNOT_WNOT" > "HOL4Vec.bword_bitop.WNOT_WNOT"
|
|
|
15 |
"WNOT_DEF" > "HOL4Vec.bword_bitop.WNOT_DEF"
|
|
|
16 |
"WCAT_WNOT" > "HOL4Vec.bword_bitop.WCAT_WNOT"
|
|
|
17 |
"WAND_DEF" > "HOL4Vec.bword_bitop.WAND_DEF"
|
|
|
18 |
"PBITOP_WNOT" > "HOL4Vec.bword_bitop.PBITOP_WNOT"
|
|
|
19 |
"PBITBOP_WXOR" > "HOL4Vec.bword_bitop.PBITBOP_WXOR"
|
|
|
20 |
"PBITBOP_WOR" > "HOL4Vec.bword_bitop.PBITBOP_WOR"
|
|
|
21 |
"PBITBOP_WAND" > "HOL4Vec.bword_bitop.PBITBOP_WAND"
|
|
|
22 |
|
|
|
23 |
end
|