|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"RIGHT_ID" > "RIGHT_ID_def"
|
|
|
7 |
"MONOID" > "MONOID_def"
|
|
|
8 |
"LEFT_ID" > "LEFT_ID_def"
|
|
|
9 |
"FCOMM" > "FCOMM_def"
|
|
|
10 |
"COMM" > "COMM_def"
|
|
|
11 |
"ASSOC" > "ASSOC_def"
|
|
|
12 |
|
|
|
13 |
const_maps
|
|
|
14 |
"RIGHT_ID" > "HOL4Base.operator.RIGHT_ID"
|
|
|
15 |
"MONOID" > "HOL4Base.operator.MONOID"
|
|
|
16 |
"LEFT_ID" > "HOL4Base.operator.LEFT_ID"
|
|
|
17 |
"FCOMM" > "HOL4Base.operator.FCOMM"
|
|
|
18 |
"COMM" > "HOL4Base.operator.COMM"
|
|
|
19 |
"ASSOC" > "HOL4Base.operator.ASSOC"
|
|
|
20 |
|
|
|
21 |
thm_maps
|
|
|
22 |
"RIGHT_ID_def" > "HOL4Base.operator.RIGHT_ID_def"
|
|
|
23 |
"RIGHT_ID_DEF" > "HOL4Base.operator.RIGHT_ID_DEF"
|
|
|
24 |
"MONOID_def" > "HOL4Base.operator.MONOID_def"
|
|
|
25 |
"MONOID_DISJ_F" > "HOL4Base.operator.MONOID_DISJ_F"
|
|
|
26 |
"MONOID_DEF" > "HOL4Base.operator.MONOID_DEF"
|
|
|
27 |
"MONOID_CONJ_T" > "HOL4Base.operator.MONOID_CONJ_T"
|
|
|
28 |
"LEFT_ID_def" > "HOL4Base.operator.LEFT_ID_def"
|
|
|
29 |
"LEFT_ID_DEF" > "HOL4Base.operator.LEFT_ID_DEF"
|
|
|
30 |
"FCOMM_def" > "HOL4Base.operator.FCOMM_def"
|
|
|
31 |
"FCOMM_DEF" > "HOL4Base.operator.FCOMM_DEF"
|
|
|
32 |
"FCOMM_ASSOC" > "HOL4Base.operator.FCOMM_ASSOC"
|
|
|
33 |
"COMM_def" > "HOL4Base.operator.COMM_def"
|
|
|
34 |
"COMM_DEF" > "HOL4Base.operator.COMM_DEF"
|
|
|
35 |
"ASSOC_def" > "HOL4Base.operator.ASSOC_def"
|
|
|
36 |
"ASSOC_DISJ" > "HOL4Base.operator.ASSOC_DISJ"
|
|
|
37 |
"ASSOC_DEF" > "HOL4Base.operator.ASSOC_DEF"
|
|
|
38 |
"ASSOC_CONJ" > "HOL4Base.operator.ASSOC_CONJ"
|
|
|
39 |
|
|
|
40 |
end
|