import
import_segment "hol4"
def_maps
"RIGHT_ID" > "RIGHT_ID_def"
"MONOID" > "MONOID_def"
"LEFT_ID" > "LEFT_ID_def"
"FCOMM" > "FCOMM_def"
"COMM" > "COMM_def"
"ASSOC" > "ASSOC_def"
const_maps
"RIGHT_ID" > "HOL4Base.operator.RIGHT_ID"
"MONOID" > "HOL4Base.operator.MONOID"
"LEFT_ID" > "HOL4Base.operator.LEFT_ID"
"FCOMM" > "HOL4Base.operator.FCOMM"
"COMM" > "HOL4Base.operator.COMM"
"ASSOC" > "HOL4Base.operator.ASSOC"
thm_maps
"RIGHT_ID_def" > "HOL4Base.operator.RIGHT_ID_def"
"RIGHT_ID_DEF" > "HOL4Base.operator.RIGHT_ID_DEF"
"MONOID_def" > "HOL4Base.operator.MONOID_def"
"MONOID_DISJ_F" > "HOL4Base.operator.MONOID_DISJ_F"
"MONOID_DEF" > "HOL4Base.operator.MONOID_DEF"
"MONOID_CONJ_T" > "HOL4Base.operator.MONOID_CONJ_T"
"LEFT_ID_def" > "HOL4Base.operator.LEFT_ID_def"
"LEFT_ID_DEF" > "HOL4Base.operator.LEFT_ID_DEF"
"FCOMM_def" > "HOL4Base.operator.FCOMM_def"
"FCOMM_DEF" > "HOL4Base.operator.FCOMM_DEF"
"FCOMM_ASSOC" > "HOL4Base.operator.FCOMM_ASSOC"
"COMM_def" > "HOL4Base.operator.COMM_def"
"COMM_DEF" > "HOL4Base.operator.COMM_DEF"
"ASSOC_def" > "HOL4Base.operator.ASSOC_def"
"ASSOC_DISJ" > "HOL4Base.operator.ASSOC_DISJ"
"ASSOC_DEF" > "HOL4Base.operator.ASSOC_DEF"
"ASSOC_CONJ" > "HOL4Base.operator.ASSOC_CONJ"
end