|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"isacut" > "isacut_def"
|
|
|
7 |
"hreal_sup" > "hreal_sup_def"
|
|
|
8 |
"hreal_sub" > "hreal_sub_def"
|
|
|
9 |
"hreal_mul" > "hreal_mul_def"
|
|
|
10 |
"hreal_lt" > "hreal_lt_def"
|
|
|
11 |
"hreal_inv" > "hreal_inv_def"
|
|
|
12 |
"hreal_add" > "hreal_add_def"
|
|
|
13 |
"hreal_1" > "hreal_1_def"
|
|
|
14 |
"hreal" > "hreal_def"
|
|
|
15 |
"hrat_lt" > "hrat_lt_def"
|
|
|
16 |
"cut_of_hrat" > "cut_of_hrat_def"
|
|
|
17 |
"cut" > "cut_def"
|
|
|
18 |
|
|
|
19 |
type_maps
|
|
|
20 |
"hreal" > "HOL4Base.hreal.hreal"
|
|
|
21 |
|
|
|
22 |
const_maps
|
|
|
23 |
"isacut" > "HOL4Base.hreal.isacut"
|
|
|
24 |
"hreal_sup" > "HOL4Base.hreal.hreal_sup"
|
|
|
25 |
"hreal_sub" > "HOL4Base.hreal.hreal_sub"
|
|
|
26 |
"hreal_mul" > "HOL4Base.hreal.hreal_mul"
|
|
|
27 |
"hreal_lt" > "HOL4Base.hreal.hreal_lt"
|
|
|
28 |
"hreal_inv" > "HOL4Base.hreal.hreal_inv"
|
|
|
29 |
"hreal_add" > "HOL4Base.hreal.hreal_add"
|
|
|
30 |
"hreal_1" > "HOL4Base.hreal.hreal_1"
|
|
|
31 |
"hrat_lt" > "HOL4Base.hreal.hrat_lt"
|
|
|
32 |
"cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
|
|
|
33 |
|
|
|
34 |
thm_maps
|
|
|
35 |
"isacut_def" > "HOL4Base.hreal.isacut_def"
|
|
|
36 |
"isacut" > "HOL4Base.hreal.isacut"
|
|
|
37 |
"hreal_tybij" > "HOL4Base.hreal.hreal_tybij"
|
|
|
38 |
"hreal_sup_def" > "HOL4Base.hreal.hreal_sup_def"
|
|
|
39 |
"hreal_sup" > "HOL4Base.hreal.hreal_sup"
|
|
|
40 |
"hreal_sub_def" > "HOL4Base.hreal.hreal_sub_def"
|
|
|
41 |
"hreal_sub" > "HOL4Base.hreal.hreal_sub"
|
|
|
42 |
"hreal_mul_def" > "HOL4Base.hreal.hreal_mul_def"
|
|
|
43 |
"hreal_mul" > "HOL4Base.hreal.hreal_mul"
|
|
|
44 |
"hreal_lt_def" > "HOL4Base.hreal.hreal_lt_def"
|
|
|
45 |
"hreal_lt" > "HOL4Base.hreal.hreal_lt"
|
|
|
46 |
"hreal_inv_def" > "HOL4Base.hreal.hreal_inv_def"
|
|
|
47 |
"hreal_inv" > "HOL4Base.hreal.hreal_inv"
|
|
|
48 |
"hreal_add_def" > "HOL4Base.hreal.hreal_add_def"
|
|
|
49 |
"hreal_add" > "HOL4Base.hreal.hreal_add"
|
|
|
50 |
"hreal_TY_DEF" > "HOL4Base.hreal.hreal_TY_DEF"
|
|
|
51 |
"hreal_1_def" > "HOL4Base.hreal.hreal_1_def"
|
|
|
52 |
"hreal_1" > "HOL4Base.hreal.hreal_1"
|
|
|
53 |
"hrat_lt_def" > "HOL4Base.hreal.hrat_lt_def"
|
|
|
54 |
"hrat_lt" > "HOL4Base.hreal.hrat_lt"
|
|
|
55 |
"cut_of_hrat_def" > "HOL4Base.hreal.cut_of_hrat_def"
|
|
|
56 |
"cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
|
|
|
57 |
"ISACUT_HRAT" > "HOL4Base.hreal.ISACUT_HRAT"
|
|
|
58 |
"HREAL_SUP_ISACUT" > "HOL4Base.hreal.HREAL_SUP_ISACUT"
|
|
|
59 |
"HREAL_SUP" > "HOL4Base.hreal.HREAL_SUP"
|
|
|
60 |
"HREAL_SUB_ISACUT" > "HOL4Base.hreal.HREAL_SUB_ISACUT"
|
|
|
61 |
"HREAL_SUB_ADD" > "HOL4Base.hreal.HREAL_SUB_ADD"
|
|
|
62 |
"HREAL_NOZERO" > "HOL4Base.hreal.HREAL_NOZERO"
|
|
|
63 |
"HREAL_MUL_SYM" > "HOL4Base.hreal.HREAL_MUL_SYM"
|
|
|
64 |
"HREAL_MUL_LINV" > "HOL4Base.hreal.HREAL_MUL_LINV"
|
|
|
65 |
"HREAL_MUL_LID" > "HOL4Base.hreal.HREAL_MUL_LID"
|
|
|
66 |
"HREAL_MUL_ISACUT" > "HOL4Base.hreal.HREAL_MUL_ISACUT"
|
|
|
67 |
"HREAL_MUL_ASSOC" > "HOL4Base.hreal.HREAL_MUL_ASSOC"
|
|
|
68 |
"HREAL_LT_TOTAL" > "HOL4Base.hreal.HREAL_LT_TOTAL"
|
|
|
69 |
"HREAL_LT_LEMMA" > "HOL4Base.hreal.HREAL_LT_LEMMA"
|
|
|
70 |
"HREAL_LT" > "HOL4Base.hreal.HREAL_LT"
|
|
|
71 |
"HREAL_LDISTRIB" > "HOL4Base.hreal.HREAL_LDISTRIB"
|
|
|
72 |
"HREAL_INV_ISACUT" > "HOL4Base.hreal.HREAL_INV_ISACUT"
|
|
|
73 |
"HREAL_ADD_TOTAL" > "HOL4Base.hreal.HREAL_ADD_TOTAL"
|
|
|
74 |
"HREAL_ADD_SYM" > "HOL4Base.hreal.HREAL_ADD_SYM"
|
|
|
75 |
"HREAL_ADD_ISACUT" > "HOL4Base.hreal.HREAL_ADD_ISACUT"
|
|
|
76 |
"HREAL_ADD_ASSOC" > "HOL4Base.hreal.HREAL_ADD_ASSOC"
|
|
|
77 |
"HRAT_UP" > "HOL4Base.hreal.HRAT_UP"
|
|
|
78 |
"HRAT_RDISTRIB" > "HOL4Base.hreal.HRAT_RDISTRIB"
|
|
|
79 |
"HRAT_MUL_RINV" > "HOL4Base.hreal.HRAT_MUL_RINV"
|
|
|
80 |
"HRAT_MUL_RID" > "HOL4Base.hreal.HRAT_MUL_RID"
|
|
|
81 |
"HRAT_MEAN" > "HOL4Base.hreal.HRAT_MEAN"
|
|
|
82 |
"HRAT_LT_TRANS" > "HOL4Base.hreal.HRAT_LT_TRANS"
|
|
|
83 |
"HRAT_LT_TOTAL" > "HOL4Base.hreal.HRAT_LT_TOTAL"
|
|
|
84 |
"HRAT_LT_RMUL1" > "HOL4Base.hreal.HRAT_LT_RMUL1"
|
|
|
85 |
"HRAT_LT_RMUL" > "HOL4Base.hreal.HRAT_LT_RMUL"
|
|
|
86 |
"HRAT_LT_REFL" > "HOL4Base.hreal.HRAT_LT_REFL"
|
|
|
87 |
"HRAT_LT_RADD" > "HOL4Base.hreal.HRAT_LT_RADD"
|
|
|
88 |
"HRAT_LT_R1" > "HOL4Base.hreal.HRAT_LT_R1"
|
|
|
89 |
"HRAT_LT_NE" > "HOL4Base.hreal.HRAT_LT_NE"
|
|
|
90 |
"HRAT_LT_MUL2" > "HOL4Base.hreal.HRAT_LT_MUL2"
|
|
|
91 |
"HRAT_LT_LMUL1" > "HOL4Base.hreal.HRAT_LT_LMUL1"
|
|
|
92 |
"HRAT_LT_LMUL" > "HOL4Base.hreal.HRAT_LT_LMUL"
|
|
|
93 |
"HRAT_LT_LADD" > "HOL4Base.hreal.HRAT_LT_LADD"
|
|
|
94 |
"HRAT_LT_L1" > "HOL4Base.hreal.HRAT_LT_L1"
|
|
|
95 |
"HRAT_LT_GT" > "HOL4Base.hreal.HRAT_LT_GT"
|
|
|
96 |
"HRAT_LT_ANTISYM" > "HOL4Base.hreal.HRAT_LT_ANTISYM"
|
|
|
97 |
"HRAT_LT_ADDR" > "HOL4Base.hreal.HRAT_LT_ADDR"
|
|
|
98 |
"HRAT_LT_ADDL" > "HOL4Base.hreal.HRAT_LT_ADDL"
|
|
|
99 |
"HRAT_LT_ADD2" > "HOL4Base.hreal.HRAT_LT_ADD2"
|
|
|
100 |
"HRAT_INV_MUL" > "HOL4Base.hreal.HRAT_INV_MUL"
|
|
|
101 |
"HRAT_GT_LMUL1" > "HOL4Base.hreal.HRAT_GT_LMUL1"
|
|
|
102 |
"HRAT_GT_L1" > "HOL4Base.hreal.HRAT_GT_L1"
|
|
|
103 |
"HRAT_EQ_LMUL" > "HOL4Base.hreal.HRAT_EQ_LMUL"
|
|
|
104 |
"HRAT_EQ_LADD" > "HOL4Base.hreal.HRAT_EQ_LADD"
|
|
|
105 |
"HRAT_DOWN2" > "HOL4Base.hreal.HRAT_DOWN2"
|
|
|
106 |
"HRAT_DOWN" > "HOL4Base.hreal.HRAT_DOWN"
|
|
|
107 |
"EQUAL_CUTS" > "HOL4Base.hreal.EQUAL_CUTS"
|
|
|
108 |
"CUT_UP" > "HOL4Base.hreal.CUT_UP"
|
|
|
109 |
"CUT_UBOUND" > "HOL4Base.hreal.CUT_UBOUND"
|
|
|
110 |
"CUT_STRADDLE" > "HOL4Base.hreal.CUT_STRADDLE"
|
|
|
111 |
"CUT_NONEMPTY" > "HOL4Base.hreal.CUT_NONEMPTY"
|
|
|
112 |
"CUT_NEARTOP_MUL" > "HOL4Base.hreal.CUT_NEARTOP_MUL"
|
|
|
113 |
"CUT_NEARTOP_ADD" > "HOL4Base.hreal.CUT_NEARTOP_ADD"
|
|
|
114 |
"CUT_ISACUT" > "HOL4Base.hreal.CUT_ISACUT"
|
|
|
115 |
"CUT_DOWN" > "HOL4Base.hreal.CUT_DOWN"
|
|
|
116 |
"CUT_BOUNDED" > "HOL4Base.hreal.CUT_BOUNDED"
|
|
|
117 |
|
|
|
118 |
end
|