import
import_segment "hol4"
def_maps
"word_size" > "word_size_primdef"
"word_case" > "word_case_primdef"
"word_base0" > "word_base0_primdef"
"mk_word" > "mk_word_def"
"dest_word" > "dest_word_def"
"bit" > "bit_def"
"WSPLIT" > "WSPLIT_def"
"WSEG" > "WSEG_def"
"WORDLEN" > "WORDLEN_def"
"WORD" > "WORD_def"
"WCAT" > "WCAT_def"
"PWORDLEN" > "PWORDLEN_primdef"
"MSB" > "MSB_def"
"LSB" > "LSB_def"
type_maps
"word" > "HOL4Vec.word_base.word"
const_maps
"word_base0" > "HOL4Vec.word_base.word_base0"
"WORD" > "HOL4Vec.word_base.WORD"
"PWORDLEN" > "HOL4Vec.word_base.PWORDLEN"
const_renames
"BIT" > "bit"
thm_maps
"word_size_def" > "HOL4Vec.word_base.word_size_def"
"word_repfns" > "HOL4Vec.word_base.word_repfns"
"word_nchotomy" > "HOL4Vec.word_base.word_nchotomy"
"word_induction" > "HOL4Vec.word_base.word_induction"
"word_induct" > "HOL4Vec.word_base.word_induct"
"word_cases" > "HOL4Vec.word_base.word_cases"
"word_case_def" > "HOL4Vec.word_base.word_case_def"
"word_case_cong" > "HOL4Vec.word_base.word_case_cong"
"word_base0_primdef" > "HOL4Vec.word_base.word_base0_primdef"
"word_base0_def" > "HOL4Vec.word_base.word_base0_def"
"word_TY_DEF" > "HOL4Vec.word_base.word_TY_DEF"
"word_Axiom" > "HOL4Vec.word_base.word_Axiom"
"word_Ax" > "HOL4Vec.word_base.word_Ax"
"word_11" > "HOL4Vec.word_base.word_11"
"WSPLIT_WSEG2" > "HOL4Vec.word_base.WSPLIT_WSEG2"
"WSPLIT_WSEG1" > "HOL4Vec.word_base.WSPLIT_WSEG1"
"WSPLIT_WSEG" > "HOL4Vec.word_base.WSPLIT_WSEG"
"WSPLIT_PWORDLEN" > "HOL4Vec.word_base.WSPLIT_PWORDLEN"
"WSPLIT_DEF" > "HOL4Vec.word_base.WSPLIT_DEF"
"WSEG_WSEG" > "HOL4Vec.word_base.WSEG_WSEG"
"WSEG_WORD_LENGTH" > "HOL4Vec.word_base.WSEG_WORD_LENGTH"
"WSEG_WORDLEN" > "HOL4Vec.word_base.WSEG_WORDLEN"
"WSEG_WCAT_WSEG2" > "HOL4Vec.word_base.WSEG_WCAT_WSEG2"
"WSEG_WCAT_WSEG1" > "HOL4Vec.word_base.WSEG_WCAT_WSEG1"
"WSEG_WCAT_WSEG" > "HOL4Vec.word_base.WSEG_WCAT_WSEG"
"WSEG_WCAT2" > "HOL4Vec.word_base.WSEG_WCAT2"
"WSEG_WCAT1" > "HOL4Vec.word_base.WSEG_WCAT1"
"WSEG_SUC" > "HOL4Vec.word_base.WSEG_SUC"
"WSEG_PWORDLEN" > "HOL4Vec.word_base.WSEG_PWORDLEN"
"WSEG_DEF" > "HOL4Vec.word_base.WSEG_DEF"
"WSEG_BIT" > "HOL4Vec.word_base.WSEG_BIT"
"WSEG0" > "HOL4Vec.word_base.WSEG0"
"WORD_def" > "HOL4Vec.word_base.WORD_def"
"WORD_SPLIT" > "HOL4Vec.word_base.WORD_SPLIT"
"WORD_SNOC_WCAT" > "HOL4Vec.word_base.WORD_SNOC_WCAT"
"WORD_PARTITION" > "HOL4Vec.word_base.WORD_PARTITION"
"WORD_CONS_WCAT" > "HOL4Vec.word_base.WORD_CONS_WCAT"
"WORD_11" > "HOL4Vec.word_base.WORD_11"
"WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT"
"WORDLEN_SUC_WCAT_WSEG_WSEG" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_WSEG_WSEG"
"WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT"
"WORDLEN_SUC_WCAT_BIT_WSEG" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT_BIT_WSEG"
"WORDLEN_SUC_WCAT" > "HOL4Vec.word_base.WORDLEN_SUC_WCAT"
"WORDLEN_DEF" > "HOL4Vec.word_base.WORDLEN_DEF"
"WORD" > "HOL4Vec.word_base.WORD"
"WCAT_WSEG_WSEG" > "HOL4Vec.word_base.WCAT_WSEG_WSEG"
"WCAT_PWORDLEN" > "HOL4Vec.word_base.WCAT_PWORDLEN"
"WCAT_DEF" > "HOL4Vec.word_base.WCAT_DEF"
"WCAT_ASSOC" > "HOL4Vec.word_base.WCAT_ASSOC"
"WCAT_11" > "HOL4Vec.word_base.WCAT_11"
"WCAT0" > "HOL4Vec.word_base.WCAT0"
"PWORDLEN_primdef" > "HOL4Vec.word_base.PWORDLEN_primdef"
"PWORDLEN_def" > "HOL4Vec.word_base.PWORDLEN_def"
"PWORDLEN1" > "HOL4Vec.word_base.PWORDLEN1"
"PWORDLEN0" > "HOL4Vec.word_base.PWORDLEN0"
"PWORDLEN" > "HOL4Vec.word_base.PWORDLEN"
"MSB_DEF" > "HOL4Vec.word_base.MSB_DEF"
"MSB" > "HOL4Vec.word_base.MSB"
"LSB_DEF" > "HOL4Vec.word_base.LSB_DEF"
"LSB" > "HOL4Vec.word_base.LSB"
"IN_PWORDLEN" > "HOL4Vec.word_base.IN_PWORDLEN"
"BIT_WSEG" > "HOL4Vec.word_base.BIT_WSEG"
"BIT_WCAT_SND" > "HOL4Vec.word_base.BIT_WCAT_SND"
"BIT_WCAT_FST" > "HOL4Vec.word_base.BIT_WCAT_FST"
"BIT_WCAT1" > "HOL4Vec.word_base.BIT_WCAT1"
"BIT_EQ_IMP_WORD_EQ" > "HOL4Vec.word_base.BIT_EQ_IMP_WORD_EQ"
"BIT_DEF" > "HOL4Vec.word_base.BIT_DEF"
"BIT0" > "HOL4Vec.word_base.BIT0"
end