import
import_segment "hol4"
def_maps
"W" > "W_def"
"S" > "S_def"
"K" > "K_def"
"I" > "I_def"
"C" > "C_def"
const_maps
"o" > "Fun.comp"
"W" > "HOL4Base.combin.W"
"S" > "HOL4Base.combin.S"
"K" > "HOL4Base.combin.K"
"I" > "HOL4Base.combin.I"
"C" > "HOL4Base.combin.C"
thm_maps
"o_THM" > "Fun.comp_def"
"o_DEF" > "Fun.comp_def"
"o_ASSOC" > "Fun.o_assoc"
"W_def" > "HOL4Base.combin.W_def"
"W_THM" > "HOL4Base.combin.W_def"
"W_DEF" > "HOL4Base.combin.W_DEF"
"S_def" > "HOL4Base.combin.S_def"
"S_THM" > "HOL4Base.combin.S_def"
"S_DEF" > "HOL4Base.combin.S_DEF"
"K_def" > "HOL4Base.combin.K_def"
"K_THM" > "HOL4Base.combin.K_def"
"K_DEF" > "HOL4Base.combin.K_DEF"
"I_o_ID" > "HOL4Base.combin.I_o_ID"
"I_def" > "HOL4Base.combin.I_def"
"I_THM" > "HOL4Base.combin.I_THM"
"I_DEF" > "HOL4Base.combin.I_DEF"
"C_def" > "HOL4Base.combin.C_def"
"C_THM" > "HOL4Base.combin.C_def"
"C_DEF" > "HOL4Base.combin.C_DEF"
end