|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"STL" > "STL_primdef"
|
|
|
7 |
"STAKE" > "STAKE_primdef"
|
|
|
8 |
"SHD" > "SHD_primdef"
|
|
|
9 |
"SDROP" > "SDROP_primdef"
|
|
|
10 |
"SDEST" > "SDEST_primdef"
|
|
|
11 |
"SCONST" > "SCONST_primdef"
|
|
|
12 |
"SCONS" > "SCONS_primdef"
|
|
|
13 |
|
|
|
14 |
const_maps
|
|
|
15 |
"STL" > "HOL4Prob.boolean_sequence.STL"
|
|
|
16 |
"SHD" > "HOL4Prob.boolean_sequence.SHD"
|
|
|
17 |
"SDEST" > "HOL4Prob.boolean_sequence.SDEST"
|
|
|
18 |
"SCONST" > "HOL4Prob.boolean_sequence.SCONST"
|
|
|
19 |
|
|
|
20 |
thm_maps
|
|
|
21 |
"STL_primdef" > "HOL4Prob.boolean_sequence.STL_primdef"
|
|
|
22 |
"STL_def" > "HOL4Prob.boolean_sequence.STL_def"
|
|
|
23 |
"STL_SCONST" > "HOL4Prob.boolean_sequence.STL_SCONST"
|
|
|
24 |
"STL_SCONS" > "HOL4Prob.boolean_sequence.STL_SCONS"
|
|
|
25 |
"STAKE_def" > "HOL4Prob.boolean_sequence.STAKE_def"
|
|
|
26 |
"SHD_primdef" > "HOL4Prob.boolean_sequence.SHD_primdef"
|
|
|
27 |
"SHD_def" > "HOL4Prob.boolean_sequence.SHD_def"
|
|
|
28 |
"SHD_STL_ISO" > "HOL4Prob.boolean_sequence.SHD_STL_ISO"
|
|
|
29 |
"SHD_SCONST" > "HOL4Prob.boolean_sequence.SHD_SCONST"
|
|
|
30 |
"SHD_SCONS" > "HOL4Prob.boolean_sequence.SHD_SCONS"
|
|
|
31 |
"SDROP_def" > "HOL4Prob.boolean_sequence.SDROP_def"
|
|
|
32 |
"SDEST_primdef" > "HOL4Prob.boolean_sequence.SDEST_primdef"
|
|
|
33 |
"SDEST_def" > "HOL4Prob.boolean_sequence.SDEST_def"
|
|
|
34 |
"SCONS_def" > "HOL4Prob.boolean_sequence.SCONS_def"
|
|
|
35 |
"SCONS_SURJ" > "HOL4Prob.boolean_sequence.SCONS_SURJ"
|
|
|
36 |
"SCONST_primdef" > "HOL4Prob.boolean_sequence.SCONST_primdef"
|
|
|
37 |
"SCONST_def" > "HOL4Prob.boolean_sequence.SCONST_def"
|
|
|
38 |
|
|
|
39 |
end
|