|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"tdiv" > "tdiv_def"
|
|
|
7 |
"tan" > "tan_def"
|
|
|
8 |
"sqrt" > "sqrt_def"
|
|
|
9 |
"sin" > "sin_def"
|
|
|
10 |
"rsum" > "rsum_def"
|
|
|
11 |
"root" > "root_def"
|
|
|
12 |
"pi" > "pi_def"
|
|
|
13 |
"ln" > "ln_def"
|
|
|
14 |
"gauge" > "gauge_def"
|
|
|
15 |
"fine" > "fine_def"
|
|
|
16 |
"exp" > "exp_def"
|
|
|
17 |
"dsize" > "dsize_def"
|
|
|
18 |
"division" > "division_def"
|
|
|
19 |
"cos" > "cos_def"
|
|
|
20 |
"atn" > "atn_def"
|
|
|
21 |
"asn" > "asn_def"
|
|
|
22 |
"acs" > "acs_def"
|
|
|
23 |
"Dint" > "Dint_def"
|
|
|
24 |
|
|
|
25 |
const_maps
|
|
|
26 |
"tdiv" > "HOL4Real.transc.tdiv"
|
|
|
27 |
"tan" > "HOL4Real.transc.tan"
|
|
|
28 |
"sqrt" > "HOL4Real.transc.sqrt"
|
|
|
29 |
"sin" > "HOL4Real.transc.sin"
|
|
|
30 |
"rsum" > "HOL4Real.transc.rsum"
|
|
|
31 |
"root" > "HOL4Real.transc.root"
|
|
|
32 |
"pi" > "HOL4Real.transc.pi"
|
|
|
33 |
"ln" > "HOL4Real.transc.ln"
|
|
|
34 |
"gauge" > "HOL4Real.transc.gauge"
|
|
|
35 |
"fine" > "HOL4Real.transc.fine"
|
|
|
36 |
"exp" > "HOL4Real.transc.exp"
|
|
|
37 |
"dsize" > "HOL4Real.transc.dsize"
|
|
|
38 |
"division" > "HOL4Real.transc.division"
|
|
|
39 |
"cos" > "HOL4Real.transc.cos"
|
|
|
40 |
"atn" > "HOL4Real.transc.atn"
|
|
|
41 |
"asn" > "HOL4Real.transc.asn"
|
|
|
42 |
"acs" > "HOL4Real.transc.acs"
|
|
|
43 |
"Dint" > "HOL4Real.transc.Dint"
|
|
|
44 |
|
|
|
45 |
thm_maps
|
|
|
46 |
"tdiv_def" > "HOL4Real.transc.tdiv_def"
|
|
|
47 |
"tdiv" > "HOL4Real.transc.tdiv"
|
|
|
48 |
"tan_def" > "HOL4Real.transc.tan_def"
|
|
|
49 |
"tan" > "HOL4Real.transc.tan"
|
|
|
50 |
"sqrt_def" > "HOL4Real.transc.sqrt_def"
|
|
|
51 |
"sqrt" > "HOL4Real.transc.sqrt"
|
|
|
52 |
"sin_def" > "HOL4Real.transc.sin_def"
|
|
|
53 |
"sin" > "HOL4Real.transc.sin"
|
|
|
54 |
"rsum_def" > "HOL4Real.transc.rsum_def"
|
|
|
55 |
"rsum" > "HOL4Real.transc.rsum"
|
|
|
56 |
"root_def" > "HOL4Real.transc.root_def"
|
|
|
57 |
"root" > "HOL4Real.transc.root"
|
|
|
58 |
"pi_def" > "HOL4Real.transc.pi_def"
|
|
|
59 |
"pi" > "HOL4Real.transc.pi"
|
|
|
60 |
"ln_def" > "HOL4Real.transc.ln_def"
|
|
|
61 |
"ln" > "HOL4Real.transc.ln"
|
|
|
62 |
"gauge_def" > "HOL4Real.transc.gauge_def"
|
|
|
63 |
"gauge" > "HOL4Real.transc.gauge"
|
|
|
64 |
"fine_def" > "HOL4Real.transc.fine_def"
|
|
|
65 |
"fine" > "HOL4Real.transc.fine"
|
|
|
66 |
"exp_def" > "HOL4Real.transc.exp_def"
|
|
|
67 |
"exp" > "HOL4Real.transc.exp"
|
|
|
68 |
"dsize_def" > "HOL4Real.transc.dsize_def"
|
|
|
69 |
"dsize" > "HOL4Real.transc.dsize"
|
|
|
70 |
"division_def" > "HOL4Real.transc.division_def"
|
|
|
71 |
"division" > "HOL4Real.transc.division"
|
|
|
72 |
"cos_def" > "HOL4Real.transc.cos_def"
|
|
|
73 |
"cos" > "HOL4Real.transc.cos"
|
|
|
74 |
"atn_def" > "HOL4Real.transc.atn_def"
|
|
|
75 |
"atn" > "HOL4Real.transc.atn"
|
|
|
76 |
"asn_def" > "HOL4Real.transc.asn_def"
|
|
|
77 |
"asn" > "HOL4Real.transc.asn"
|
|
|
78 |
"acs_def" > "HOL4Real.transc.acs_def"
|
|
|
79 |
"acs" > "HOL4Real.transc.acs"
|
|
|
80 |
"TAN_TOTAL_POS" > "HOL4Real.transc.TAN_TOTAL_POS"
|
|
|
81 |
"TAN_TOTAL_LEMMA" > "HOL4Real.transc.TAN_TOTAL_LEMMA"
|
|
|
82 |
"TAN_TOTAL" > "HOL4Real.transc.TAN_TOTAL"
|
|
|
83 |
"TAN_SEC" > "HOL4Real.transc.TAN_SEC"
|
|
|
84 |
"TAN_POS_PI2" > "HOL4Real.transc.TAN_POS_PI2"
|
|
|
85 |
"TAN_PI" > "HOL4Real.transc.TAN_PI"
|
|
|
86 |
"TAN_PERIODIC" > "HOL4Real.transc.TAN_PERIODIC"
|
|
|
87 |
"TAN_NPI" > "HOL4Real.transc.TAN_NPI"
|
|
|
88 |
"TAN_NEG" > "HOL4Real.transc.TAN_NEG"
|
|
|
89 |
"TAN_DOUBLE" > "HOL4Real.transc.TAN_DOUBLE"
|
|
|
90 |
"TAN_ATN" > "HOL4Real.transc.TAN_ATN"
|
|
|
91 |
"TAN_ADD" > "HOL4Real.transc.TAN_ADD"
|
|
|
92 |
"TAN_0" > "HOL4Real.transc.TAN_0"
|
|
|
93 |
"SQRT_POW_2" > "HOL4Real.transc.SQRT_POW_2"
|
|
|
94 |
"SQRT_POW2" > "HOL4Real.transc.SQRT_POW2"
|
|
|
95 |
"SQRT_POS_UNIQ" > "HOL4Real.transc.SQRT_POS_UNIQ"
|
|
|
96 |
"SQRT_POS_LT" > "HOL4Real.transc.SQRT_POS_LT"
|
|
|
97 |
"SQRT_POS_LE" > "HOL4Real.transc.SQRT_POS_LE"
|
|
|
98 |
"SQRT_MUL" > "HOL4Real.transc.SQRT_MUL"
|
|
|
99 |
"SQRT_MONO_LE" > "HOL4Real.transc.SQRT_MONO_LE"
|
|
|
100 |
"SQRT_INV" > "HOL4Real.transc.SQRT_INV"
|
|
|
101 |
"SQRT_EVEN_POW2" > "HOL4Real.transc.SQRT_EVEN_POW2"
|
|
|
102 |
"SQRT_EQ" > "HOL4Real.transc.SQRT_EQ"
|
|
|
103 |
"SQRT_DIV" > "HOL4Real.transc.SQRT_DIV"
|
|
|
104 |
"SQRT_1" > "HOL4Real.transc.SQRT_1"
|
|
|
105 |
"SQRT_0" > "HOL4Real.transc.SQRT_0"
|
|
|
106 |
"SIN_ZERO_LEMMA" > "HOL4Real.transc.SIN_ZERO_LEMMA"
|
|
|
107 |
"SIN_ZERO" > "HOL4Real.transc.SIN_ZERO"
|
|
|
108 |
"SIN_TOTAL" > "HOL4Real.transc.SIN_TOTAL"
|
|
|
109 |
"SIN_POS_PI_LE" > "HOL4Real.transc.SIN_POS_PI_LE"
|
|
|
110 |
"SIN_POS_PI2_LE" > "HOL4Real.transc.SIN_POS_PI2_LE"
|
|
|
111 |
"SIN_POS_PI2" > "HOL4Real.transc.SIN_POS_PI2"
|
|
|
112 |
"SIN_POS_PI" > "HOL4Real.transc.SIN_POS_PI"
|
|
|
113 |
"SIN_POS" > "HOL4Real.transc.SIN_POS"
|
|
|
114 |
"SIN_PI2" > "HOL4Real.transc.SIN_PI2"
|
|
|
115 |
"SIN_PI" > "HOL4Real.transc.SIN_PI"
|
|
|
116 |
"SIN_PERIODIC_PI" > "HOL4Real.transc.SIN_PERIODIC_PI"
|
|
|
117 |
"SIN_PERIODIC" > "HOL4Real.transc.SIN_PERIODIC"
|
|
|
118 |
"SIN_PAIRED" > "HOL4Real.transc.SIN_PAIRED"
|
|
|
119 |
"SIN_NPI" > "HOL4Real.transc.SIN_NPI"
|
|
|
120 |
"SIN_NEGLEMMA" > "HOL4Real.transc.SIN_NEGLEMMA"
|
|
|
121 |
"SIN_NEG" > "HOL4Real.transc.SIN_NEG"
|
|
|
122 |
"SIN_FDIFF" > "HOL4Real.transc.SIN_FDIFF"
|
|
|
123 |
"SIN_DOUBLE" > "HOL4Real.transc.SIN_DOUBLE"
|
|
|
124 |
"SIN_COS_SQRT" > "HOL4Real.transc.SIN_COS_SQRT"
|
|
|
125 |
"SIN_COS_SQ" > "HOL4Real.transc.SIN_COS_SQ"
|
|
|
126 |
"SIN_COS_NEG" > "HOL4Real.transc.SIN_COS_NEG"
|
|
|
127 |
"SIN_COS_ADD" > "HOL4Real.transc.SIN_COS_ADD"
|
|
|
128 |
"SIN_COS" > "HOL4Real.transc.SIN_COS"
|
|
|
129 |
"SIN_CONVERGES" > "HOL4Real.transc.SIN_CONVERGES"
|
|
|
130 |
"SIN_CIRCLE" > "HOL4Real.transc.SIN_CIRCLE"
|
|
|
131 |
"SIN_BOUNDS" > "HOL4Real.transc.SIN_BOUNDS"
|
|
|
132 |
"SIN_BOUND" > "HOL4Real.transc.SIN_BOUND"
|
|
|
133 |
"SIN_ASN" > "HOL4Real.transc.SIN_ASN"
|
|
|
134 |
"SIN_ADD" > "HOL4Real.transc.SIN_ADD"
|
|
|
135 |
"SIN_ACS_NZ" > "HOL4Real.transc.SIN_ACS_NZ"
|
|
|
136 |
"SIN_0" > "HOL4Real.transc.SIN_0"
|
|
|
137 |
"ROOT_POW_POS" > "HOL4Real.transc.ROOT_POW_POS"
|
|
|
138 |
"ROOT_POS_UNIQ" > "HOL4Real.transc.ROOT_POS_UNIQ"
|
|
|
139 |
"ROOT_POS_LT" > "HOL4Real.transc.ROOT_POS_LT"
|
|
|
140 |
"ROOT_POS" > "HOL4Real.transc.ROOT_POS"
|
|
|
141 |
"ROOT_MUL" > "HOL4Real.transc.ROOT_MUL"
|
|
|
142 |
"ROOT_MONO_LE" > "HOL4Real.transc.ROOT_MONO_LE"
|
|
|
143 |
"ROOT_LT_LEMMA" > "HOL4Real.transc.ROOT_LT_LEMMA"
|
|
|
144 |
"ROOT_LN" > "HOL4Real.transc.ROOT_LN"
|
|
|
145 |
"ROOT_INV" > "HOL4Real.transc.ROOT_INV"
|
|
|
146 |
"ROOT_DIV" > "HOL4Real.transc.ROOT_DIV"
|
|
|
147 |
"ROOT_1" > "HOL4Real.transc.ROOT_1"
|
|
|
148 |
"ROOT_0" > "HOL4Real.transc.ROOT_0"
|
|
|
149 |
"REAL_DIV_SQRT" > "HOL4Real.transc.REAL_DIV_SQRT"
|
|
|
150 |
"POW_ROOT_POS" > "HOL4Real.transc.POW_ROOT_POS"
|
|
|
151 |
"POW_2_SQRT" > "HOL4Real.transc.POW_2_SQRT"
|
|
|
152 |
"PI_POS" > "HOL4Real.transc.PI_POS"
|
|
|
153 |
"PI2_BOUNDS" > "HOL4Real.transc.PI2_BOUNDS"
|
|
|
154 |
"PI2" > "HOL4Real.transc.PI2"
|
|
|
155 |
"MCLAURIN_ZERO" > "HOL4Real.transc.MCLAURIN_ZERO"
|
|
|
156 |
"MCLAURIN_NEG" > "HOL4Real.transc.MCLAURIN_NEG"
|
|
|
157 |
"MCLAURIN_EXP_LT" > "HOL4Real.transc.MCLAURIN_EXP_LT"
|
|
|
158 |
"MCLAURIN_EXP_LE" > "HOL4Real.transc.MCLAURIN_EXP_LE"
|
|
|
159 |
"MCLAURIN_ALL_LT" > "HOL4Real.transc.MCLAURIN_ALL_LT"
|
|
|
160 |
"MCLAURIN_ALL_LE" > "HOL4Real.transc.MCLAURIN_ALL_LE"
|
|
|
161 |
"MCLAURIN" > "HOL4Real.transc.MCLAURIN"
|
|
|
162 |
"LN_POW" > "HOL4Real.transc.LN_POW"
|
|
|
163 |
"LN_POS" > "HOL4Real.transc.LN_POS"
|
|
|
164 |
"LN_MUL" > "HOL4Real.transc.LN_MUL"
|
|
|
165 |
"LN_MONO_LT" > "HOL4Real.transc.LN_MONO_LT"
|
|
|
166 |
"LN_MONO_LE" > "HOL4Real.transc.LN_MONO_LE"
|
|
|
167 |
"LN_LT_X" > "HOL4Real.transc.LN_LT_X"
|
|
|
168 |
"LN_LE" > "HOL4Real.transc.LN_LE"
|
|
|
169 |
"LN_INV" > "HOL4Real.transc.LN_INV"
|
|
|
170 |
"LN_INJ" > "HOL4Real.transc.LN_INJ"
|
|
|
171 |
"LN_EXP" > "HOL4Real.transc.LN_EXP"
|
|
|
172 |
"LN_DIV" > "HOL4Real.transc.LN_DIV"
|
|
|
173 |
"LN_1" > "HOL4Real.transc.LN_1"
|
|
|
174 |
"INTEGRAL_NULL" > "HOL4Real.transc.INTEGRAL_NULL"
|
|
|
175 |
"GAUGE_MIN" > "HOL4Real.transc.GAUGE_MIN"
|
|
|
176 |
"FTC1" > "HOL4Real.transc.FTC1"
|
|
|
177 |
"FINE_MIN" > "HOL4Real.transc.FINE_MIN"
|
|
|
178 |
"EXP_TOTAL_LEMMA" > "HOL4Real.transc.EXP_TOTAL_LEMMA"
|
|
|
179 |
"EXP_TOTAL" > "HOL4Real.transc.EXP_TOTAL"
|
|
|
180 |
"EXP_SUB" > "HOL4Real.transc.EXP_SUB"
|
|
|
181 |
"EXP_POS_LT" > "HOL4Real.transc.EXP_POS_LT"
|
|
|
182 |
"EXP_POS_LE" > "HOL4Real.transc.EXP_POS_LE"
|
|
|
183 |
"EXP_NZ" > "HOL4Real.transc.EXP_NZ"
|
|
|
184 |
"EXP_NEG_MUL2" > "HOL4Real.transc.EXP_NEG_MUL2"
|
|
|
185 |
"EXP_NEG_MUL" > "HOL4Real.transc.EXP_NEG_MUL"
|
|
|
186 |
"EXP_NEG" > "HOL4Real.transc.EXP_NEG"
|
|
|
187 |
"EXP_N" > "HOL4Real.transc.EXP_N"
|
|
|
188 |
"EXP_MONO_LT" > "HOL4Real.transc.EXP_MONO_LT"
|
|
|
189 |
"EXP_MONO_LE" > "HOL4Real.transc.EXP_MONO_LE"
|
|
|
190 |
"EXP_MONO_IMP" > "HOL4Real.transc.EXP_MONO_IMP"
|
|
|
191 |
"EXP_LT_1" > "HOL4Real.transc.EXP_LT_1"
|
|
|
192 |
"EXP_LN" > "HOL4Real.transc.EXP_LN"
|
|
|
193 |
"EXP_LE_X" > "HOL4Real.transc.EXP_LE_X"
|
|
|
194 |
"EXP_INJ" > "HOL4Real.transc.EXP_INJ"
|
|
|
195 |
"EXP_FDIFF" > "HOL4Real.transc.EXP_FDIFF"
|
|
|
196 |
"EXP_CONVERGES" > "HOL4Real.transc.EXP_CONVERGES"
|
|
|
197 |
"EXP_ADD_MUL" > "HOL4Real.transc.EXP_ADD_MUL"
|
|
|
198 |
"EXP_ADD" > "HOL4Real.transc.EXP_ADD"
|
|
|
199 |
"EXP_0" > "HOL4Real.transc.EXP_0"
|
|
|
200 |
"Dint_def" > "HOL4Real.transc.Dint_def"
|
|
|
201 |
"Dint" > "HOL4Real.transc.Dint"
|
|
|
202 |
"DIVISION_UBOUND_LT" > "HOL4Real.transc.DIVISION_UBOUND_LT"
|
|
|
203 |
"DIVISION_UBOUND" > "HOL4Real.transc.DIVISION_UBOUND"
|
|
|
204 |
"DIVISION_THM" > "HOL4Real.transc.DIVISION_THM"
|
|
|
205 |
"DIVISION_SINGLE" > "HOL4Real.transc.DIVISION_SINGLE"
|
|
|
206 |
"DIVISION_RHS" > "HOL4Real.transc.DIVISION_RHS"
|
|
|
207 |
"DIVISION_LT_GEN" > "HOL4Real.transc.DIVISION_LT_GEN"
|
|
|
208 |
"DIVISION_LT" > "HOL4Real.transc.DIVISION_LT"
|
|
|
209 |
"DIVISION_LHS" > "HOL4Real.transc.DIVISION_LHS"
|
|
|
210 |
"DIVISION_LE" > "HOL4Real.transc.DIVISION_LE"
|
|
|
211 |
"DIVISION_LBOUND_LT" > "HOL4Real.transc.DIVISION_LBOUND_LT"
|
|
|
212 |
"DIVISION_LBOUND" > "HOL4Real.transc.DIVISION_LBOUND"
|
|
|
213 |
"DIVISION_GT" > "HOL4Real.transc.DIVISION_GT"
|
|
|
214 |
"DIVISION_EXISTS" > "HOL4Real.transc.DIVISION_EXISTS"
|
|
|
215 |
"DIVISION_EQ" > "HOL4Real.transc.DIVISION_EQ"
|
|
|
216 |
"DIVISION_APPEND" > "HOL4Real.transc.DIVISION_APPEND"
|
|
|
217 |
"DIVISION_1" > "HOL4Real.transc.DIVISION_1"
|
|
|
218 |
"DIVISION_0" > "HOL4Real.transc.DIVISION_0"
|
|
|
219 |
"DINT_UNIQ" > "HOL4Real.transc.DINT_UNIQ"
|
|
|
220 |
"DIFF_TAN" > "HOL4Real.transc.DIFF_TAN"
|
|
|
221 |
"DIFF_SIN" > "HOL4Real.transc.DIFF_SIN"
|
|
|
222 |
"DIFF_LN_COMPOSITE" > "HOL4Real.transc.DIFF_LN_COMPOSITE"
|
|
|
223 |
"DIFF_LN" > "HOL4Real.transc.DIFF_LN"
|
|
|
224 |
"DIFF_EXP" > "HOL4Real.transc.DIFF_EXP"
|
|
|
225 |
"DIFF_COS" > "HOL4Real.transc.DIFF_COS"
|
|
|
226 |
"DIFF_COMPOSITE" > "HOL4Real.transc.DIFF_COMPOSITE"
|
|
|
227 |
"DIFF_ATN" > "HOL4Real.transc.DIFF_ATN"
|
|
|
228 |
"DIFF_ASN_LEMMA" > "HOL4Real.transc.DIFF_ASN_LEMMA"
|
|
|
229 |
"DIFF_ASN" > "HOL4Real.transc.DIFF_ASN"
|
|
|
230 |
"DIFF_ACS_LEMMA" > "HOL4Real.transc.DIFF_ACS_LEMMA"
|
|
|
231 |
"DIFF_ACS" > "HOL4Real.transc.DIFF_ACS"
|
|
|
232 |
"COS_ZERO_LEMMA" > "HOL4Real.transc.COS_ZERO_LEMMA"
|
|
|
233 |
"COS_ZERO" > "HOL4Real.transc.COS_ZERO"
|
|
|
234 |
"COS_TOTAL" > "HOL4Real.transc.COS_TOTAL"
|
|
|
235 |
"COS_SIN_SQRT" > "HOL4Real.transc.COS_SIN_SQRT"
|
|
|
236 |
"COS_SIN_SQ" > "HOL4Real.transc.COS_SIN_SQ"
|
|
|
237 |
"COS_SIN" > "HOL4Real.transc.COS_SIN"
|
|
|
238 |
"COS_POS_PI_LE" > "HOL4Real.transc.COS_POS_PI_LE"
|
|
|
239 |
"COS_POS_PI2_LE" > "HOL4Real.transc.COS_POS_PI2_LE"
|
|
|
240 |
"COS_POS_PI2" > "HOL4Real.transc.COS_POS_PI2"
|
|
|
241 |
"COS_POS_PI" > "HOL4Real.transc.COS_POS_PI"
|
|
|
242 |
"COS_PI2" > "HOL4Real.transc.COS_PI2"
|
|
|
243 |
"COS_PI" > "HOL4Real.transc.COS_PI"
|
|
|
244 |
"COS_PERIODIC_PI" > "HOL4Real.transc.COS_PERIODIC_PI"
|
|
|
245 |
"COS_PERIODIC" > "HOL4Real.transc.COS_PERIODIC"
|
|
|
246 |
"COS_PAIRED" > "HOL4Real.transc.COS_PAIRED"
|
|
|
247 |
"COS_NPI" > "HOL4Real.transc.COS_NPI"
|
|
|
248 |
"COS_NEG" > "HOL4Real.transc.COS_NEG"
|
|
|
249 |
"COS_ISZERO" > "HOL4Real.transc.COS_ISZERO"
|
|
|
250 |
"COS_FDIFF" > "HOL4Real.transc.COS_FDIFF"
|
|
|
251 |
"COS_DOUBLE" > "HOL4Real.transc.COS_DOUBLE"
|
|
|
252 |
"COS_CONVERGES" > "HOL4Real.transc.COS_CONVERGES"
|
|
|
253 |
"COS_BOUNDS" > "HOL4Real.transc.COS_BOUNDS"
|
|
|
254 |
"COS_BOUND" > "HOL4Real.transc.COS_BOUND"
|
|
|
255 |
"COS_ATN_NZ" > "HOL4Real.transc.COS_ATN_NZ"
|
|
|
256 |
"COS_ASN_NZ" > "HOL4Real.transc.COS_ASN_NZ"
|
|
|
257 |
"COS_ADD" > "HOL4Real.transc.COS_ADD"
|
|
|
258 |
"COS_ACS" > "HOL4Real.transc.COS_ACS"
|
|
|
259 |
"COS_2" > "HOL4Real.transc.COS_2"
|
|
|
260 |
"COS_0" > "HOL4Real.transc.COS_0"
|
|
|
261 |
"ATN_TAN" > "HOL4Real.transc.ATN_TAN"
|
|
|
262 |
"ATN_BOUNDS" > "HOL4Real.transc.ATN_BOUNDS"
|
|
|
263 |
"ATN" > "HOL4Real.transc.ATN"
|
|
|
264 |
"ASN_SIN" > "HOL4Real.transc.ASN_SIN"
|
|
|
265 |
"ASN_BOUNDS_LT" > "HOL4Real.transc.ASN_BOUNDS_LT"
|
|
|
266 |
"ASN_BOUNDS" > "HOL4Real.transc.ASN_BOUNDS"
|
|
|
267 |
"ASN" > "HOL4Real.transc.ASN"
|
|
|
268 |
"ACS_COS" > "HOL4Real.transc.ACS_COS"
|
|
|
269 |
"ACS_BOUNDS_LT" > "HOL4Real.transc.ACS_BOUNDS_LT"
|
|
|
270 |
"ACS_BOUNDS" > "HOL4Real.transc.ACS_BOUNDS"
|
|
|
271 |
"ACS" > "HOL4Real.transc.ACS"
|
|
|
272 |
|
|
|
273 |
end
|