|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"word_size" > "word_size_primdef"
|
|
|
7 |
"word_case" > "word_case_primdef"
|
|
|
8 |
"word_base0" > "word_base0_primdef"
|
|
|
9 |
"mk_word" > "mk_word_def"
|
|
|
10 |
"dest_word" > "dest_word_def"
|
|
|
11 |
"bit" > "bit_def"
|
|
|
12 |
"WSPLIT" > "WSPLIT_def"
|
|
|
13 |
"WSEG" > "WSEG_def"
|
|
|
14 |
"WORDLEN" > "WORDLEN_def"
|
|
|
15 |
"WORD" > "WORD_def"
|
|
|
16 |
"WCAT" > "WCAT_def"
|
|
|
17 |
"PWORDLEN" > "PWORDLEN_primdef"
|
|
|
18 |
"MSB" > "MSB_def"
|
|
|
19 |
"LSB" > "LSB_def"
|
|
|
20 |
|
|
|
21 |
type_maps
|
|
|
22 |
"word" > "HOL4Vec.word_base.word"
|
|
|
23 |
|
|
|
24 |
const_maps
|
|
|
25 |
"word_base0" > "HOL4Vec.word_base.word_base0"
|
|
|
26 |
"WORD" > "HOL4Vec.word_base.WORD"
|
|
|
27 |
"PWORDLEN" > "HOL4Vec.word_base.PWORDLEN"
|
|
|
28 |
|
|
|
29 |
const_renames
|
|
|
30 |
"BIT" > "bit"
|
|
|
31 |
|
|
|
32 |
thm_maps
|
|
|
33 |
"word_size_def" > "HOL4Vec.word_base.word_size_def"
|
|
|
34 |
"word_repfns" > "HOL4Vec.word_base.word_repfns"
|
|
|
35 |
"word_nchotomy" > "HOL4Vec.word_base.word_nchotomy"
|
|
|
36 |
"word_induction" > "HOL4Vec.word_base.word_induction"
|
|
|
37 |
"word_induct" > "HOL4Vec.word_base.word_induct"
|
|
|
38 |
"word_cases" > "HOL4Vec.word_base.word_cases"
|
|
|
39 |
"word_case_def" > "HOL4Vec.word_base.word_case_def"
|
|
|
40 |
"word_case_cong" > "HOL4Vec.word_base.word_case_cong"
|
|
|
41 |
"word_base0_primdef" > "HOL4Vec.word_base.word_base0_primdef"
|
|
|
42 |
"word_base0_def" > "HOL4Vec.word_base.word_base0_def"
|
|
|
43 |
"word_TY_DEF" > "HOL4Vec.word_base.word_TY_DEF"
|
|
|
44 |
"word_Axiom" > "HOL4Vec.word_base.word_Axiom"
|
|
|
45 |
"word_Ax" > "HOL4Vec.word_base.word_Ax"
|
|
|
46 |
"word_11" > "HOL4Vec.word_base.word_11"
|
|
|
47 |
"WSPLIT_WSEG2" > "HOL4Vec.word_base.WSPLIT_WSEG2"
|
|
|
48 |
"WSPLIT_WSEG1" > "HOL4Vec.word_base.WSPLIT_WSEG1"
|
|
|
49 |
"WSPLIT_WSEG" > "HOL4Vec.word_base.WSPLIT_WSEG"
|
|
|
50 |
"WSPLIT_PWORDLEN" > "HOL4Vec.word_base.WSPLIT_PWORDLEN"
|
|
|
51 |
"WSPLIT_DEF" > "HOL4Vec.word_base.WSPLIT_DEF"
|
|
|
52 |
"WSEG_WSEG" > "HOL4Vec.word_base.WSEG_WSEG"
|
|
|
53 |
"WSEG_WORD_LENGTH" > "HOL4Vec.word_base.WSEG_WORD_LENGTH"
|
|
|
54 |
"WSEG_WORDLEN" > "HOL4Vec.word_base.WSEG_WORDLEN"
|
|
|
55 |
"WSEG_WCAT_WSEG2" > "HOL4Vec.word_base.WSEG_WCAT_WSEG2"
|
|
|
56 |
"WSEG_WCAT_WSEG1" > "HOL4Vec.word_base.WSEG_WCAT_WSEG1"
|
|
|
57 |
"WSEG_WCAT_WSEG" > "HOL4Vec.word_base.WSEG_WCAT_WSEG"
|
|
|
58 |
"WSEG_WCAT2" > "HOL4Vec.word_base.WSEG_WCAT2"
|
|
|
59 |
"WSEG_WCAT1" > "HOL4Vec.word_base.WSEG_WCAT1"
|
|
|
60 |
"WSEG_SUC" > "HOL4Vec.word_base.WSEG_SUC"
|
|
|
61 |
"WSEG_PWORDLEN" > "HOL4Vec.word_base.WSEG_PWORDLEN"
|
|
|
62 |
"WSEG_DEF" > "HOL4Vec.word_base.WSEG_DEF"
|
|
|
63 |
"WSEG_BIT" > "HOL4Vec.word_base.WSEG_BIT"
|
|
|
64 |
"WSEG0" > "HOL4Vec.word_base.WSEG0"
|
|
|
65 |
"WORD_def" > "HOL4Vec.word_base.WORD_def"
|
|
|
66 |
"WORD_SPLIT" > "HOL4Vec.word_base.WORD_SPLIT"
|
|
|
67 |
"WORD_SNOC_WCAT" > "HOL4Vec.word_base.WORD_SNOC_WCAT"
|
|
|
68 |
"WORD_PARTITION" > "HOL4Vec.word_base.WORD_PARTITION"
|
|
|
69 |
"WORD_CONS_WCAT" > "HOL4Vec.word_base.WORD_CONS_WCAT"
|
|
|
70 |
"WORD_11" > "HOL4Vec.word_base.WORD_11"
|
|
|
71 |
"WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT"
|
|
|
72 |
"WORDLEN_SUC_WCAT_WSEG_WSEG" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_WSEG_WSEG"
|
|
|
73 |
"WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT"
|
|
|
74 |
"WORDLEN_SUC_WCAT_BIT_WSEG" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_BIT_WSEG"
|
|
|
75 |
"WORDLEN_SUC_WCAT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT"
|
|
|
76 |
"WORDLEN_DEF" > "HOL4Vec.word_base.WORDLEN_DEF"
|
|
|
77 |
"WORD" > "HOL4Vec.word_base.WORD"
|
|
|
78 |
"WCAT_WSEG_WSEG" > "HOL4Vec.word_base.WCAT_WSEG_WSEG"
|
|
|
79 |
"WCAT_PWORDLEN" > "HOL4Vec.word_base.WCAT_PWORDLEN"
|
|
|
80 |
"WCAT_DEF" > "HOL4Vec.word_base.WCAT_DEF"
|
|
|
81 |
"WCAT_ASSOC" > "HOL4Vec.word_base.WCAT_ASSOC"
|
|
|
82 |
"WCAT_11" > "HOL4Vec.word_base.WCAT_11"
|
|
|
83 |
"WCAT0" > "HOL4Vec.word_base.WCAT0"
|
|
|
84 |
"PWORDLEN_primdef" > "HOL4Vec.word_base.PWORDLEN_primdef"
|
|
|
85 |
"PWORDLEN_def" > "HOL4Vec.word_base.PWORDLEN_def"
|
|
|
86 |
"PWORDLEN1" > "HOL4Vec.word_base.PWORDLEN1"
|
|
|
87 |
"PWORDLEN0" > "HOL4Vec.word_base.PWORDLEN0"
|
|
|
88 |
"PWORDLEN" > "HOL4Vec.word_base.PWORDLEN"
|
|
|
89 |
"MSB_DEF" > "HOL4Vec.word_base.MSB_DEF"
|
|
|
90 |
"MSB" > "HOL4Vec.word_base.MSB"
|
|
|
91 |
"LSB_DEF" > "HOL4Vec.word_base.LSB_DEF"
|
|
|
92 |
"LSB" > "HOL4Vec.word_base.LSB"
|
|
|
93 |
"IN_PWORDLEN" > "HOL4Vec.word_base.IN_PWORDLEN"
|
|
|
94 |
"BIT_WSEG" > "HOL4Vec.word_base.BIT_WSEG"
|
|
|
95 |
"BIT_WCAT_SND" > "HOL4Vec.word_base.BIT_WCAT_SND"
|
|
|
96 |
"BIT_WCAT_FST" > "HOL4Vec.word_base.BIT_WCAT_FST"
|
|
|
97 |
"BIT_WCAT1" > "HOL4Vec.word_base.BIT_WCAT1"
|
|
|
98 |
"BIT_EQ_IMP_WORD_EQ" > "HOL4Vec.word_base.BIT_EQ_IMP_WORD_EQ"
|
|
|
99 |
"BIT_DEF" > "HOL4Vec.word_base.BIT_DEF"
|
|
|
100 |
"BIT0" > "HOL4Vec.word_base.BIT0"
|
|
|
101 |
|
|
|
102 |
end
|