|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"mk_rec" > "mk_rec_def"
|
|
|
7 |
"dest_rec" > "dest_rec_def"
|
|
|
8 |
"ZRECSPACE" > "ZRECSPACE_def"
|
|
|
9 |
"ZCONSTR" > "ZCONSTR_def"
|
|
|
10 |
"ZBOT" > "ZBOT_def"
|
|
|
11 |
"NUMSUM" > "NUMSUM_def"
|
|
|
12 |
"NUMSND" > "NUMSND_def"
|
|
|
13 |
"NUMRIGHT" > "NUMRIGHT_def"
|
|
|
14 |
"NUMPAIR" > "NUMPAIR_def"
|
|
|
15 |
"NUMLEFT" > "NUMLEFT_def"
|
|
|
16 |
"NUMFST" > "NUMFST_def"
|
|
|
17 |
"ISO" > "ISO_def"
|
|
|
18 |
"INJP" > "INJP_def"
|
|
|
19 |
"INJN" > "INJN_def"
|
|
|
20 |
"INJF" > "INJF_def"
|
|
|
21 |
"INJA" > "INJA_def"
|
|
|
22 |
"FNIL" > "FNIL_def"
|
|
|
23 |
"FCONS" > "FCONS_def"
|
|
|
24 |
"CONSTR" > "CONSTR_def"
|
|
|
25 |
"BOTTOM" > "BOTTOM_def"
|
|
|
26 |
|
|
|
27 |
type_maps
|
|
|
28 |
"recspace" > "HOL4Base.ind_type.recspace"
|
|
|
29 |
|
|
|
30 |
const_maps
|
|
|
31 |
"ZRECSPACE" > "HOL4Base.ind_type.ZRECSPACE"
|
|
|
32 |
"ZCONSTR" > "HOL4Base.ind_type.ZCONSTR"
|
|
|
33 |
"ZBOT" > "HOL4Base.ind_type.ZBOT"
|
|
|
34 |
"NUMSUM" > "HOL4Base.ind_type.NUMSUM"
|
|
|
35 |
"NUMPAIR" > "HOL4Base.ind_type.NUMPAIR"
|
|
|
36 |
"ISO" > "HOL4Base.ind_type.ISO"
|
|
|
37 |
"INJP" > "HOL4Base.ind_type.INJP"
|
|
|
38 |
"INJN" > "HOL4Base.ind_type.INJN"
|
|
|
39 |
"INJF" > "HOL4Base.ind_type.INJF"
|
|
|
40 |
"INJA" > "HOL4Base.ind_type.INJA"
|
|
|
41 |
"FNIL" > "HOL4Base.ind_type.FNIL"
|
|
|
42 |
"CONSTR" > "HOL4Base.ind_type.CONSTR"
|
|
|
43 |
"BOTTOM" > "HOL4Base.ind_type.BOTTOM"
|
|
|
44 |
|
|
|
45 |
thm_maps
|
|
|
46 |
"recspace_repfns" > "HOL4Base.ind_type.recspace_repfns"
|
|
|
47 |
"recspace_TY_DEF" > "HOL4Base.ind_type.recspace_TY_DEF"
|
|
|
48 |
"ZRECSPACE_rules" > "HOL4Base.ind_type.ZRECSPACE_rules"
|
|
|
49 |
"ZRECSPACE_ind" > "HOL4Base.ind_type.ZRECSPACE_ind"
|
|
|
50 |
"ZRECSPACE_def" > "HOL4Base.ind_type.ZRECSPACE_def"
|
|
|
51 |
"ZRECSPACE_cases" > "HOL4Base.ind_type.ZRECSPACE_cases"
|
|
|
52 |
"ZRECSPACE" > "HOL4Base.ind_type.ZRECSPACE"
|
|
|
53 |
"ZCONSTR_def" > "HOL4Base.ind_type.ZCONSTR_def"
|
|
|
54 |
"ZCONSTR_ZBOT" > "HOL4Base.ind_type.ZCONSTR_ZBOT"
|
|
|
55 |
"ZCONSTR" > "HOL4Base.ind_type.ZCONSTR"
|
|
|
56 |
"ZBOT_def" > "HOL4Base.ind_type.ZBOT_def"
|
|
|
57 |
"ZBOT" > "HOL4Base.ind_type.ZBOT"
|
|
|
58 |
"NUMSUM_def" > "HOL4Base.ind_type.NUMSUM_def"
|
|
|
59 |
"NUMSUM_INJ" > "HOL4Base.ind_type.NUMSUM_INJ"
|
|
|
60 |
"NUMSUM_DEST" > "HOL4Base.ind_type.NUMSUM_DEST"
|
|
|
61 |
"NUMSUM" > "HOL4Base.ind_type.NUMSUM"
|
|
|
62 |
"NUMPAIR_def" > "HOL4Base.ind_type.NUMPAIR_def"
|
|
|
63 |
"NUMPAIR_INJ_LEMMA" > "HOL4Base.ind_type.NUMPAIR_INJ_LEMMA"
|
|
|
64 |
"NUMPAIR_INJ" > "HOL4Base.ind_type.NUMPAIR_INJ"
|
|
|
65 |
"NUMPAIR_DEST" > "HOL4Base.ind_type.NUMPAIR_DEST"
|
|
|
66 |
"NUMPAIR" > "HOL4Base.ind_type.NUMPAIR"
|
|
|
67 |
"MK_REC_INJ" > "HOL4Base.ind_type.MK_REC_INJ"
|
|
|
68 |
"ISO_def" > "HOL4Base.ind_type.ISO_def"
|
|
|
69 |
"ISO_USAGE" > "HOL4Base.ind_type.ISO_USAGE"
|
|
|
70 |
"ISO_REFL" > "HOL4Base.ind_type.ISO_REFL"
|
|
|
71 |
"ISO_FUN" > "HOL4Base.ind_type.ISO_FUN"
|
|
|
72 |
"ISO" > "HOL4Base.ind_type.ISO"
|
|
|
73 |
"INJ_INVERSE2" > "HOL4Base.ind_type.INJ_INVERSE2"
|
|
|
74 |
"INJP_def" > "HOL4Base.ind_type.INJP_def"
|
|
|
75 |
"INJP_INJ" > "HOL4Base.ind_type.INJP_INJ"
|
|
|
76 |
"INJP" > "HOL4Base.ind_type.INJP"
|
|
|
77 |
"INJN_def" > "HOL4Base.ind_type.INJN_def"
|
|
|
78 |
"INJN_INJ" > "HOL4Base.ind_type.INJN_INJ"
|
|
|
79 |
"INJN" > "HOL4Base.ind_type.INJN"
|
|
|
80 |
"INJF_def" > "HOL4Base.ind_type.INJF_def"
|
|
|
81 |
"INJF_INJ" > "HOL4Base.ind_type.INJF_INJ"
|
|
|
82 |
"INJF" > "HOL4Base.ind_type.INJF"
|
|
|
83 |
"INJA_def" > "HOL4Base.ind_type.INJA_def"
|
|
|
84 |
"INJA_INJ" > "HOL4Base.ind_type.INJA_INJ"
|
|
|
85 |
"INJA" > "HOL4Base.ind_type.INJA"
|
|
|
86 |
"FNIL_def" > "HOL4Base.ind_type.FNIL_def"
|
|
|
87 |
"FNIL" > "HOL4Base.ind_type.FNIL"
|
|
|
88 |
"FCONS" > "HOL4Base.ind_type.FCONS"
|
|
|
89 |
"DEST_REC_INJ" > "HOL4Base.ind_type.DEST_REC_INJ"
|
|
|
90 |
"CONSTR_def" > "HOL4Base.ind_type.CONSTR_def"
|
|
|
91 |
"CONSTR_REC" > "HOL4Base.ind_type.CONSTR_REC"
|
|
|
92 |
"CONSTR_INJ" > "HOL4Base.ind_type.CONSTR_INJ"
|
|
|
93 |
"CONSTR_IND" > "HOL4Base.ind_type.CONSTR_IND"
|
|
|
94 |
"CONSTR_BOT" > "HOL4Base.ind_type.CONSTR_BOT"
|
|
|
95 |
"CONSTR" > "HOL4Base.ind_type.CONSTR"
|
|
|
96 |
"BOTTOM_def" > "HOL4Base.ind_type.BOTTOM_def"
|
|
|
97 |
"BOTTOM" > "HOL4Base.ind_type.BOTTOM"
|
|
|
98 |
|
|
|
99 |
end
|