|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"trat_sucint" > "trat_sucint_def"
|
|
|
7 |
"trat_mul" > "trat_mul_def"
|
|
|
8 |
"trat_inv" > "trat_inv_def"
|
|
|
9 |
"trat_eq" > "trat_eq_def"
|
|
|
10 |
"trat_add" > "trat_add_def"
|
|
|
11 |
"trat_1" > "trat_1_def"
|
|
|
12 |
"mk_hrat" > "mk_hrat_def"
|
|
|
13 |
"hrat_sucint" > "hrat_sucint_def"
|
|
|
14 |
"hrat_mul" > "hrat_mul_def"
|
|
|
15 |
"hrat_inv" > "hrat_inv_def"
|
|
|
16 |
"hrat_add" > "hrat_add_def"
|
|
|
17 |
"hrat_1" > "hrat_1_def"
|
|
|
18 |
"dest_hrat" > "dest_hrat_def"
|
|
|
19 |
|
|
|
20 |
type_maps
|
|
|
21 |
"hrat" > "HOL4Base.hrat.hrat"
|
|
|
22 |
|
|
|
23 |
const_maps
|
|
|
24 |
"trat_mul" > "HOL4Base.hrat.trat_mul"
|
|
|
25 |
"trat_inv" > "HOL4Base.hrat.trat_inv"
|
|
|
26 |
"trat_eq" > "HOL4Base.hrat.trat_eq"
|
|
|
27 |
"trat_add" > "HOL4Base.hrat.trat_add"
|
|
|
28 |
"trat_1" > "HOL4Base.hrat.trat_1"
|
|
|
29 |
"hrat_sucint" > "HOL4Base.hrat.hrat_sucint"
|
|
|
30 |
"hrat_mul" > "HOL4Base.hrat.hrat_mul"
|
|
|
31 |
"hrat_inv" > "HOL4Base.hrat.hrat_inv"
|
|
|
32 |
"hrat_add" > "HOL4Base.hrat.hrat_add"
|
|
|
33 |
"hrat_1" > "HOL4Base.hrat.hrat_1"
|
|
|
34 |
|
|
|
35 |
thm_maps
|
|
|
36 |
"trat_sucint" > "HOL4Base.hrat.trat_sucint"
|
|
|
37 |
"trat_mul_def" > "HOL4Base.hrat.trat_mul_def"
|
|
|
38 |
"trat_mul" > "HOL4Base.hrat.trat_mul"
|
|
|
39 |
"trat_inv_def" > "HOL4Base.hrat.trat_inv_def"
|
|
|
40 |
"trat_inv" > "HOL4Base.hrat.trat_inv"
|
|
|
41 |
"trat_eq_def" > "HOL4Base.hrat.trat_eq_def"
|
|
|
42 |
"trat_eq" > "HOL4Base.hrat.trat_eq"
|
|
|
43 |
"trat_add_def" > "HOL4Base.hrat.trat_add_def"
|
|
|
44 |
"trat_add" > "HOL4Base.hrat.trat_add"
|
|
|
45 |
"trat_1_def" > "HOL4Base.hrat.trat_1_def"
|
|
|
46 |
"trat_1" > "HOL4Base.hrat.trat_1"
|
|
|
47 |
"hrat_tybij" > "HOL4Base.hrat.hrat_tybij"
|
|
|
48 |
"hrat_sucint_def" > "HOL4Base.hrat.hrat_sucint_def"
|
|
|
49 |
"hrat_sucint" > "HOL4Base.hrat.hrat_sucint"
|
|
|
50 |
"hrat_mul_def" > "HOL4Base.hrat.hrat_mul_def"
|
|
|
51 |
"hrat_mul" > "HOL4Base.hrat.hrat_mul"
|
|
|
52 |
"hrat_inv_def" > "HOL4Base.hrat.hrat_inv_def"
|
|
|
53 |
"hrat_inv" > "HOL4Base.hrat.hrat_inv"
|
|
|
54 |
"hrat_add_def" > "HOL4Base.hrat.hrat_add_def"
|
|
|
55 |
"hrat_add" > "HOL4Base.hrat.hrat_add"
|
|
|
56 |
"hrat_TY_DEF" > "HOL4Base.hrat.hrat_TY_DEF"
|
|
|
57 |
"hrat_1_def" > "HOL4Base.hrat.hrat_1_def"
|
|
|
58 |
"hrat_1" > "HOL4Base.hrat.hrat_1"
|
|
|
59 |
"TRAT_SUCINT_0" > "HOL4Base.hrat.TRAT_SUCINT_0"
|
|
|
60 |
"TRAT_SUCINT" > "HOL4Base.hrat.TRAT_SUCINT"
|
|
|
61 |
"TRAT_NOZERO" > "HOL4Base.hrat.TRAT_NOZERO"
|
|
|
62 |
"TRAT_MUL_WELLDEFINED2" > "HOL4Base.hrat.TRAT_MUL_WELLDEFINED2"
|
|
|
63 |
"TRAT_MUL_WELLDEFINED" > "HOL4Base.hrat.TRAT_MUL_WELLDEFINED"
|
|
|
64 |
"TRAT_MUL_SYM_EQ" > "HOL4Base.hrat.TRAT_MUL_SYM_EQ"
|
|
|
65 |
"TRAT_MUL_SYM" > "HOL4Base.hrat.TRAT_MUL_SYM"
|
|
|
66 |
"TRAT_MUL_LINV" > "HOL4Base.hrat.TRAT_MUL_LINV"
|
|
|
67 |
"TRAT_MUL_LID" > "HOL4Base.hrat.TRAT_MUL_LID"
|
|
|
68 |
"TRAT_MUL_ASSOC" > "HOL4Base.hrat.TRAT_MUL_ASSOC"
|
|
|
69 |
"TRAT_LDISTRIB" > "HOL4Base.hrat.TRAT_LDISTRIB"
|
|
|
70 |
"TRAT_INV_WELLDEFINED" > "HOL4Base.hrat.TRAT_INV_WELLDEFINED"
|
|
|
71 |
"TRAT_EQ_TRANS" > "HOL4Base.hrat.TRAT_EQ_TRANS"
|
|
|
72 |
"TRAT_EQ_SYM" > "HOL4Base.hrat.TRAT_EQ_SYM"
|
|
|
73 |
"TRAT_EQ_REFL" > "HOL4Base.hrat.TRAT_EQ_REFL"
|
|
|
74 |
"TRAT_EQ_EQUIV" > "HOL4Base.hrat.TRAT_EQ_EQUIV"
|
|
|
75 |
"TRAT_EQ_AP" > "HOL4Base.hrat.TRAT_EQ_AP"
|
|
|
76 |
"TRAT_ARCH" > "HOL4Base.hrat.TRAT_ARCH"
|
|
|
77 |
"TRAT_ADD_WELLDEFINED2" > "HOL4Base.hrat.TRAT_ADD_WELLDEFINED2"
|
|
|
78 |
"TRAT_ADD_WELLDEFINED" > "HOL4Base.hrat.TRAT_ADD_WELLDEFINED"
|
|
|
79 |
"TRAT_ADD_TOTAL" > "HOL4Base.hrat.TRAT_ADD_TOTAL"
|
|
|
80 |
"TRAT_ADD_SYM_EQ" > "HOL4Base.hrat.TRAT_ADD_SYM_EQ"
|
|
|
81 |
"TRAT_ADD_SYM" > "HOL4Base.hrat.TRAT_ADD_SYM"
|
|
|
82 |
"TRAT_ADD_ASSOC" > "HOL4Base.hrat.TRAT_ADD_ASSOC"
|
|
|
83 |
"HRAT_SUCINT" > "HOL4Base.hrat.HRAT_SUCINT"
|
|
|
84 |
"HRAT_NOZERO" > "HOL4Base.hrat.HRAT_NOZERO"
|
|
|
85 |
"HRAT_MUL_SYM" > "HOL4Base.hrat.HRAT_MUL_SYM"
|
|
|
86 |
"HRAT_MUL_LINV" > "HOL4Base.hrat.HRAT_MUL_LINV"
|
|
|
87 |
"HRAT_MUL_LID" > "HOL4Base.hrat.HRAT_MUL_LID"
|
|
|
88 |
"HRAT_MUL_ASSOC" > "HOL4Base.hrat.HRAT_MUL_ASSOC"
|
|
|
89 |
"HRAT_LDISTRIB" > "HOL4Base.hrat.HRAT_LDISTRIB"
|
|
|
90 |
"HRAT_ARCH" > "HOL4Base.hrat.HRAT_ARCH"
|
|
|
91 |
"HRAT_ADD_TOTAL" > "HOL4Base.hrat.HRAT_ADD_TOTAL"
|
|
|
92 |
"HRAT_ADD_SYM" > "HOL4Base.hrat.HRAT_ADD_SYM"
|
|
|
93 |
"HRAT_ADD_ASSOC" > "HOL4Base.hrat.HRAT_ADD_ASSOC"
|
|
|
94 |
|
|
|
95 |
end
|