renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
3 import_segment "hollight"
6 "vector" > "vector_def"
7 "treal_of_num" > "treal_of_num_def"
8 "treal_neg" > "treal_neg_def"
9 "treal_mul" > "treal_mul_def"
10 "treal_le" > "treal_le_def"
11 "treal_inv" > "treal_inv_def"
12 "treal_eq" > "treal_eq_def"
13 "treal_add" > "treal_add_def"
14 "tailadmissible" > "tailadmissible_def"
15 "support" > "support_def"
16 "superadmissible" > "superadmissible_def"
18 "sndcart" > "sndcart_def"
20 "real_sub" > "real_sub_def"
21 "real_sgn" > "real_sgn_def"
22 "real_pow" > "real_pow_def"
23 "real_of_num" > "real_of_num_def"
24 "real_neg" > "real_neg_def"
25 "real_mul" > "real_mul_def"
26 "real_mod" > "real_mod_def"
27 "real_min" > "real_min_def"
28 "real_max" > "real_max_def"
29 "real_lt" > "real_lt_def"
30 "real_le" > "real_le_def"
31 "real_inv" > "real_inv_def"
32 "real_gt" > "real_gt_def"
33 "real_ge" > "real_ge_def"
34 "real_div" > "real_div_def"
35 "real_add" > "real_add_def"
36 "real_abs" > "real_abs_def"
37 "pastecart" > "pastecart_def"
38 "pairwise" > "pairwise_def"
39 "num_of_int" > "num_of_int_def"
40 "num_mod" > "num_mod_def"
41 "num_gcd" > "num_gcd_def"
42 "num_divides" > "num_divides_def"
43 "num_coprime" > "num_coprime_def"
45 "neutral" > "neutral_def"
46 "nadd_rinv" > "nadd_rinv_def"
47 "nadd_of_num" > "nadd_of_num_def"
48 "nadd_mul" > "nadd_mul_def"
49 "nadd_le" > "nadd_le_def"
50 "nadd_inv" > "nadd_inv_def"
51 "nadd_eq" > "nadd_eq_def"
52 "nadd_add" > "nadd_add_def"
53 "monoidal" > "monoidal_def"
54 "minimal" > "minimal_def"
55 "lambda" > "lambda_def"
56 "iterate" > "iterate_def"
57 "is_nadd" > "is_nadd_def"
58 "integer" > "integer_def"
59 "int_sub" > "int_sub_def"
60 "int_sgn" > "int_sgn_def"
61 "int_pow" > "int_pow_def"
62 "int_of_num" > "int_of_num_def"
63 "int_neg" > "int_neg_def"
64 "int_mul" > "int_mul_def"
65 "int_mod" > "int_mod_def"
66 "int_min" > "int_min_def"
67 "int_max" > "int_max_def"
68 "int_lt" > "int_lt_def"
69 "int_le" > "int_le_def"
70 "int_gt" > "int_gt_def"
71 "int_ge" > "int_ge_def"
72 "int_gcd" > "int_gcd_def"
73 "int_divides" > "int_divides_def"
74 "int_coprime" > "int_coprime_def"
75 "int_add" > "int_add_def"
76 "int_abs" > "int_abs_def"
77 "hreal_of_num" > "hreal_of_num_def"
78 "hreal_mul" > "hreal_mul_def"
79 "hreal_le" > "hreal_le_def"
80 "hreal_inv" > "hreal_inv_def"
81 "hreal_add" > "hreal_add_def"
82 "fstcart" > "fstcart_def"
86 "dimindex" > "dimindex_def"
87 "admissible" > "admissible_def"
88 "_UNGUARDED_PATTERN" > "_UNGUARDED_PATTERN_def"
89 "_SEQPATTERN" > "_SEQPATTERN_def"
90 "_MATCH" > "_MATCH_def"
91 "_GUARDED_PATTERN" > "_GUARDED_PATTERN_def"
92 "_FUNCTION" > "_FUNCTION_def"
93 "_FALSITY_" > "_FALSITY__def"
94 "_11937" > "_11937_def"
95 "ZRECSPACE" > "ZRECSPACE_def"
96 "ZCONSTR" > "ZCONSTR_def"
98 "UNCURRY" > "UNCURRY_def"
102 "PASSOC" > "PASSOC_def"
103 "PAIRWISE" > "PAIRWISE_def"
104 "NUM_REP" > "NUM_REP_def"
105 "NUMSUM" > "NUMSUM_def"
106 "NUMSND" > "NUMSND_def"
107 "NUMRIGHT" > "NUMRIGHT_def"
108 "NUMPAIR" > "NUMPAIR_def"
109 "NUMLEFT" > "NUMLEFT_def"
110 "NUMFST" > "NUMFST_def"
111 "LET_END" > "LET_END_def"
112 "ITSET" > "ITSET_def"
119 "IND_SUC" > "IND_SUC_def"
120 "IND_0" > "IND_0_def"
121 "HAS_SIZE" > "HAS_SIZE_def"
123 "FINREC" > "FINREC_def"
124 "FCONS" > "FCONS_def"
125 "DECIMAL" > "DECIMAL_def"
126 "CROSS" > "CROSS_def"
127 "COUNTABLE" > "COUNTABLE_def"
128 "CONSTR" > "CONSTR_def"
129 "CASEWISE" > "CASEWISE_def"
131 "BOTTOM" > "BOTTOM_def"
133 "ASCII" > "ASCII_def"
142 "sum" > "Sum_Type.sum"
143 "recspace" > "HOLLight.hollight.recspace"
144 "real" > "HOLLight.hollight.real"
145 "prod" > "Product_Type.prod"
146 "option" > "Datatype.option"
148 "nadd" > "HOLLight.hollight.nadd"
150 "int" > "HOLLight.hollight.int"
152 "hreal" > "HOLLight.hollight.hreal"
154 "finite_sum" > "HOLLight.hollight.finite_sum"
155 "finite_image" > "HOLLight.hollight.finite_image"
156 "char" > "HOLLight.hollight.char"
157 "cart" > "HOLLight.hollight.cart"
159 "N_3" > "HOLLight.hollight.N_3"
160 "N_2" > "HOLLight.hollight.N_2"
161 "N_1" > "Product_Type.unit"
165 "vector" > "HOLLight.hollight.vector"
166 "treal_of_num" > "HOLLight.hollight.treal_of_num"
167 "treal_neg" > "HOLLight.hollight.treal_neg"
168 "treal_mul" > "HOLLight.hollight.treal_mul"
169 "treal_le" > "HOLLight.hollight.treal_le"
170 "treal_inv" > "HOLLight.hollight.treal_inv"
171 "treal_eq" > "HOLLight.hollight.treal_eq"
172 "treal_add" > "HOLLight.hollight.treal_add"
173 "tailadmissible" > "HOLLight.hollight.tailadmissible"
174 "support" > "HOLLight.hollight.support"
175 "superadmissible" > "HOLLight.hollight.superadmissible"
176 "sum" > "HOLLight.hollight.sum"
177 "sndcart" > "HOLLight.hollight.sndcart"
178 "set_of_list" > "List.set"
179 "rem" > "HOLLight.hollight.rem"
180 "real_sub" > "HOLLight.hollight.real_sub"
181 "real_sgn" > "HOLLight.hollight.real_sgn"
182 "real_pow" > "HOLLight.hollight.real_pow"
183 "real_of_num" > "HOLLight.hollight.real_of_num"
184 "real_neg" > "HOLLight.hollight.real_neg"
185 "real_mul" > "HOLLight.hollight.real_mul"
186 "real_mod" > "HOLLight.hollight.real_mod"
187 "real_min" > "HOLLight.hollight.real_min"
188 "real_max" > "HOLLight.hollight.real_max"
189 "real_lt" > "HOLLight.hollight.real_lt"
190 "real_le" > "HOLLight.hollight.real_le"
191 "real_inv" > "HOLLight.hollight.real_inv"
192 "real_gt" > "HOLLight.hollight.real_gt"
193 "real_ge" > "HOLLight.hollight.real_ge"
194 "real_div" > "HOLLight.hollight.real_div"
195 "real_add" > "HOLLight.hollight.real_add"
196 "real_abs" > "HOLLight.hollight.real_abs"
197 "pastecart" > "HOLLight.hollight.pastecart"
198 "pairwise" > "HOLLight.hollight.pairwise"
199 "one" > "Product_Type.Unity"
201 "num_of_int" > "HOLLight.hollight.num_of_int"
202 "num_mod" > "HOLLight.hollight.num_mod"
203 "num_gcd" > "HOLLight.hollight.num_gcd"
204 "num_divides" > "HOLLight.hollight.num_divides"
205 "num_coprime" > "HOLLight.hollight.num_coprime"
206 "nsum" > "HOLLight.hollight.nsum"
207 "neutral" > "HOLLight.hollight.neutral"
208 "nadd_rinv" > "HOLLight.hollight.nadd_rinv"
209 "nadd_of_num" > "HOLLight.hollight.nadd_of_num"
210 "nadd_mul" > "HOLLight.hollight.nadd_mul"
211 "nadd_le" > "HOLLight.hollight.nadd_le"
212 "nadd_inv" > "HOLLight.hollight.nadd_inv"
213 "nadd_eq" > "HOLLight.hollight.nadd_eq"
214 "nadd_add" > "HOLLight.hollight.nadd_add"
215 "monoidal" > "HOLLight.hollight.monoidal"
216 "mk_pair" > "Product_Type.Pair_Rep"
218 "minimal" > "HOLLight.hollight.minimal"
219 "list_EX" > "List.list_ex"
220 "list_ALL" > "List.list_all"
221 "lambda" > "HOLLight.hollight.lambda"
222 "iterate" > "HOLLight.hollight.iterate"
223 "is_nadd" > "HOLLight.hollight.is_nadd"
224 "integer" > "HOLLight.hollight.integer"
225 "int_sub" > "HOLLight.hollight.int_sub"
226 "int_sgn" > "HOLLight.hollight.int_sgn"
227 "int_pow" > "HOLLight.hollight.int_pow"
228 "int_of_num" > "HOLLight.hollight.int_of_num"
229 "int_neg" > "HOLLight.hollight.int_neg"
230 "int_mul" > "HOLLight.hollight.int_mul"
231 "int_mod" > "HOLLight.hollight.int_mod"
232 "int_min" > "HOLLight.hollight.int_min"
233 "int_max" > "HOLLight.hollight.int_max"
234 "int_lt" > "HOLLight.hollight.int_lt"
235 "int_le" > "HOLLight.hollight.int_le"
236 "int_gt" > "HOLLight.hollight.int_gt"
237 "int_ge" > "HOLLight.hollight.int_ge"
238 "int_gcd" > "HOLLight.hollight.int_gcd"
239 "int_divides" > "HOLLight.hollight.int_divides"
240 "int_coprime" > "HOLLight.hollight.int_coprime"
241 "int_add" > "HOLLight.hollight.int_add"
242 "int_abs" > "HOLLight.hollight.int_abs"
243 "hreal_of_num" > "HOLLight.hollight.hreal_of_num"
244 "hreal_mul" > "HOLLight.hollight.hreal_mul"
245 "hreal_le" > "HOLLight.hollight.hreal_le"
246 "hreal_inv" > "HOLLight.hollight.hreal_inv"
247 "hreal_add" > "HOLLight.hollight.hreal_add"
248 "fstcart" > "HOLLight.hollight.fstcart"
249 "eqeq" > "HOLLight.hollight.eqeq"
250 "div" > "HOLLight.hollight.div"
251 "dist" > "HOLLight.hollight.dist"
252 "dimindex" > "HOLLight.hollight.dimindex"
253 "admissible" > "HOLLight.hollight.admissible"
254 "_UNGUARDED_PATTERN" > "HOLLight.hollight._UNGUARDED_PATTERN"
255 "_SEQPATTERN" > "HOLLight.hollight._SEQPATTERN"
256 "_MATCH" > "HOLLight.hollight._MATCH"
257 "_GUARDED_PATTERN" > "HOLLight.hollight._GUARDED_PATTERN"
258 "_FUNCTION" > "HOLLight.hollight._FUNCTION"
259 "_FALSITY_" > "HOLLight.hollight._FALSITY_"
260 "_11937" > "HOLLight.hollight._11937"
261 "_0" > "Groups.zero_class.zero" :: "nat"
263 "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
265 "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
266 "ZBOT" > "HOLLight.hollight.ZBOT"
267 "WF" > "Wellfounded.wfP"
268 "UNIV" > "Orderings.top_class.top" :: "'a => bool"
269 "UNIONS" > "Complete_Lattices.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
270 "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
271 "UNCURRY" > "HOLLight.hollight.UNCURRY"
274 "SURJ" > "HOLLight.hollight.SURJ"
276 "SUBSET" > "Orderings.ord_class.less_eq" :: "('a => bool) => ('a => bool) => bool"
277 "SOME" > "Datatype.Some"
278 "SND" > "Product_Type.snd"
279 "SING" > "HOLLight.hollight.SING"
280 "SETSPEC" > "HOLLightCompat.SETSPEC"
281 "REVERSE" > "List.rev"
282 "REST" > "HOLLight.hollight.REST"
283 "REPLICATE" > "List.replicate"
284 "PSUBSET" > "Orderings.ord_class.less" :: "('a => bool) => ('a => bool) => bool"
285 "PRE" > "HOLLightCompat.Pred"
286 "PASSOC" > "HOLLight.hollight.PASSOC"
287 "PAIRWISE" > "HOLLight.hollight.PAIRWISE"
288 "OUTR" > "HOLLightCompat.OUTR"
289 "OUTL" > "HOLLightCompat.OUTL"
291 "ONE_ONE" > "Fun.inj"
292 "ODD" > "HOLLightCompat.ODD"
293 "NUM_REP" > "HOLLight.hollight.NUM_REP"
294 "NUMSUM" > "HOLLight.hollight.NUMSUM"
295 "NUMSND" > "HOLLight.hollight.NUMSND"
296 "NUMRIGHT" > "HOLLight.hollight.NUMRIGHT"
297 "NUMPAIR" > "HOLLight.hollight.NUMPAIR"
298 "NUMLEFT" > "HOLLight.hollight.NUMLEFT"
299 "NUMFST" > "HOLLight.hollight.NUMFST"
300 "NUMERAL" > "HOLLightCompat.NUMERAL"
302 "NONE" > "Datatype.None"
303 "NIL" > "List.list.Nil"
304 "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
305 "MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
306 "MEM" > "HOLLightList.list_mem"
307 "MEASURE" > "HOLLightCompat.MEASURE"
308 "MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
309 "MAP2" > "HOLLightList.map2"
311 "LET_END" > "HOLLight.hollight.LET_END"
312 "LET" > "HOLLightCompat.LET"
313 "LENGTH" > "List.length"
315 "ITSET" > "HOLLight.hollight.ITSET"
316 "ITLIST2" > "HOLLightList.fold2"
317 "ITLIST" > "List.foldr"
318 "ISO" > "HOLLight.hollight.ISO"
319 "INTERS" > "Complete_Lattices.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
320 "INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
321 "INSERT" > "Set.insert"
322 "INR" > "Sum_Type.Inr"
323 "INL" > "Sum_Type.Inl"
324 "INJP" > "HOLLight.hollight.INJP"
325 "INJN" > "HOLLight.hollight.INJN"
326 "INJF" > "HOLLight.hollight.INJF"
327 "INJA" > "HOLLight.hollight.INJA"
328 "INJ" > "HOLLight.hollight.INJ"
329 "INFINITE" > "HOLLightCompat.INFINITE"
330 "IND_SUC" > "HOLLight.hollight.IND_SUC"
331 "IND_0" > "HOLLight.hollight.IND_0"
333 "IMAGE" > "Set.image"
336 "HAS_SIZE" > "HOLLight.hollight.HAS_SIZE"
337 "GSPEC" > "Set.Collect"
339 "GABS" > "Hilbert_Choice.Eps"
340 "FST" > "Product_Type.fst"
341 "FNIL" > "HOLLight.hollight.FNIL"
342 "FINREC" > "HOLLight.hollight.FINREC"
343 "FINITE" > "Finite_Set.finite"
344 "FILTER" > "List.filter"
345 "FCONS" > "HOLLight.hollight.FCONS"
346 "FACT" > "Fact.fact_class.fact" :: "nat => nat"
348 "EXP" > "Power.power_class.power" :: "nat => nat => nat"
349 "EVEN" > "Parity.even_odd_class.even" :: "nat => bool"
350 "EMPTY" > "Orderings.bot_class.bot" :: "'a => bool"
351 "EL" > "HOLLightList.list_el"
352 "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
353 "DISJOINT" > "HOLLightCompat.DISJOINT"
354 "DIFF" > "Groups.minus_class.minus" :: "('a => bool) => ('a => bool) => 'a => bool"
355 "DELETE" > "HOLLightCompat.DELETE"
356 "DECIMAL" > "HOLLight.hollight.DECIMAL"
357 "CURRY" > "Product_Type.curry"
358 "CROSS" > "HOLLight.hollight.CROSS"
359 "COUNTABLE" > "HOLLight.hollight.COUNTABLE"
360 "CONSTR" > "HOLLight.hollight.CONSTR"
361 "CONS" > "List.list.Cons"
363 "CHOICE" > "Hilbert_Choice.Eps"
364 "CASEWISE" > "HOLLight.hollight.CASEWISE"
365 "CARD" > "HOLLight.hollight.CARD"
366 "BUTLAST" > "List.butlast"
367 "BOTTOM" > "HOLLight.hollight.BOTTOM"
368 "BIT1" > "HOLLightCompat.NUMERAL_BIT1"
369 "BIT0" > "HOLLightCompat.NUMERAL_BIT0"
370 "BIJ" > "HOLLight.hollight.BIJ"
371 "ASCII" > "HOLLight.hollight.ASCII"
372 "APPEND" > "List.append"
373 "ALL2" > "List.list_all2"
374 "@" > "Hilbert_Choice.Eps"
377 ">_c" > "HOLLight.hollight.>_c"
378 ">=_c" > "HOLLight.hollight.>=_c"
379 ">=" > "Orderings.ord_class.greater_eq" :: "nat => nat => bool"
380 ">" > "Orderings.ord_class.greater" :: "nat => nat => bool"
381 "=_c" > "HOLLight.hollight.=_c"
382 "==>" > "HOL.implies"
384 "<_c" > "HOLLight.hollight.<_c"
385 "<=_c" > "HOLLight.hollight.<=_c"
386 "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
387 "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
389 ".." > "HOLLightCompat.dotdot"
390 "-" > "Groups.minus_class.minus" :: "nat => nat => nat"
391 "," > "Product_Type.Pair"
392 "+" > "Groups.plus_class.plus" :: "nat => nat => nat"
393 "*" > "Groups.times_class.times" :: "nat => nat => nat"
394 "$" > "HOLLight.hollight.$"
403 "vector_def" > "HOLLight.hollight.vector_def"
404 "treal_of_num_def" > "HOLLight.hollight.treal_of_num_def"
405 "treal_neg_def" > "HOLLight.hollight.treal_neg_def"
406 "treal_mul_def" > "HOLLight.hollight.treal_mul_def"
407 "treal_le_def" > "HOLLight.hollight.treal_le_def"
408 "treal_inv_def" > "HOLLight.hollight.treal_inv_def"
409 "treal_eq_def" > "HOLLight.hollight.treal_eq_def"
410 "treal_add_def" > "HOLLight.hollight.treal_add_def"
411 "th_cond" > "HOLLight.hollight.th_cond"
412 "th" > "HOL.eta_contract_eq"
413 "tailadmissible_def" > "HOLLight.hollight.tailadmissible_def"
414 "support_def" > "HOLLight.hollight.support_def"
415 "superadmissible_def" > "HOLLight.hollight.superadmissible_def"
416 "sum_def" > "HOLLight.hollight.sum_def"
417 "string_INFINITE" > "List.infinite_UNIV_listI"
418 "sth" > "HOLLight.hollight.sth"
419 "sndcart_def" > "HOLLight.hollight.sndcart_def"
420 "right_th" > "HOLLight.hollight.right_th"
421 "rem_def" > "HOLLight.hollight.rem_def"
422 "real_sub_def" > "HOLLight.hollight.real_sub_def"
423 "real_sgn_def" > "HOLLight.hollight.real_sgn_def"
424 "real_pow_def" > "HOLLight.hollight.real_pow_def"
425 "real_of_num_def" > "HOLLight.hollight.real_of_num_def"
426 "real_neg_def" > "HOLLight.hollight.real_neg_def"
427 "real_mul_def" > "HOLLight.hollight.real_mul_def"
428 "real_mod_def" > "HOLLight.hollight.real_mod_def"
429 "real_min_def" > "HOLLight.hollight.real_min_def"
430 "real_max_def" > "HOLLight.hollight.real_max_def"
431 "real_lt_def" > "HOLLight.hollight.real_lt_def"
432 "real_le_def" > "HOLLight.hollight.real_le_def"
433 "real_inv_def" > "HOLLight.hollight.real_inv_def"
434 "real_gt_def" > "HOLLight.hollight.real_gt_def"
435 "real_ge_def" > "HOLLight.hollight.real_ge_def"
436 "real_div_def" > "HOLLight.hollight.real_div_def"
437 "real_add_def" > "HOLLight.hollight.real_add_def"
438 "real_abs_def" > "HOLLight.hollight.real_abs_def"
439 "real_INFINITE" > "HOLLight.hollight.real_INFINITE"
440 "pastecart_def" > "HOLLight.hollight.pastecart_def"
441 "pairwise_def" > "HOLLight.hollight.pairwise_def"
442 "pair_RECURSION" > "HOLLight.hollight.pair_RECURSION"
443 "pair_INDUCT" > "Product_Type.prod.induct"
444 "one_axiom" > "HOLLight.hollight.one_axiom"
445 "one_RECURSION" > "HOLLight.hollight.one_RECURSION"
446 "one_INDUCT" > "Product_Type.unit.induct"
447 "one_Axiom" > "HOLLight.hollight.one_Axiom"
448 "one" > "HOLLightCompat.one"
449 "o_THM" > "Fun.comp_def"
450 "o_ASSOC" > "HOLLight.hollight.o_ASSOC"
451 "num_of_int_def" > "HOLLight.hollight.num_of_int_def"
452 "num_mod_def" > "HOLLight.hollight.num_mod_def"
453 "num_gcd_def" > "HOLLight.hollight.num_gcd_def"
454 "num_divides_def" > "HOLLight.hollight.num_divides_def"
455 "num_coprime_def" > "HOLLight.hollight.num_coprime_def"
456 "num_congruent" > "HOLLight.hollight.num_congruent"
457 "num_WOP" > "HOLLight.hollight.num_WOP"
458 "num_WF" > "Nat.nat_less_induct"
459 "num_RECURSION_STD" > "HOLLight.hollight.num_RECURSION_STD"
460 "num_MAX" > "HOLLight.hollight.num_MAX"
461 "num_INFINITE" > "Finite_Set.infinite_UNIV_char_0"
462 "num_INDUCTION" > "Fact.fact_nat.induct"
463 "num_FINITE_AVOID" > "HOLLight.hollight.num_FINITE_AVOID"
464 "num_FINITE" > "HOLLight.hollight.num_FINITE"
465 "num_CASES" > "Nat.nat.nchotomy"
466 "num_Axiom" > "HOLLightCompat.num_Axiom"
467 "nsum_def" > "HOLLight.hollight.nsum_def"
468 "neutral_def" > "HOLLight.hollight.neutral_def"
469 "nadd_rinv_def" > "HOLLight.hollight.nadd_rinv_def"
470 "nadd_of_num_def" > "HOLLight.hollight.nadd_of_num_def"
471 "nadd_mul_def" > "HOLLight.hollight.nadd_mul_def"
472 "nadd_le_def" > "HOLLight.hollight.nadd_le_def"
473 "nadd_inv_def" > "HOLLight.hollight.nadd_inv_def"
474 "nadd_eq_def" > "HOLLight.hollight.nadd_eq_def"
475 "nadd_add_def" > "HOLLight.hollight.nadd_add_def"
476 "monoidal_def" > "HOLLight.hollight.monoidal_def"
477 "minimal_def" > "HOLLight.hollight.minimal_def"
478 "list_INDUCT" > "List.list.induct"
479 "list_CASES" > "List.list.nchotomy"
480 "lambda_def" > "HOLLight.hollight.lambda_def"
481 "iterate_def" > "HOLLight.hollight.iterate_def"
482 "is_nadd_def" > "HOLLight.hollight.is_nadd_def"
483 "is_nadd_0" > "HOLLight.hollight.is_nadd_0"
484 "is_int" > "HOLLight.hollight.is_int"
485 "integer_def" > "HOLLight.hollight.integer_def"
486 "int_sub_th" > "HOLLight.hollight.int_sub_th"
487 "int_sub_def" > "HOLLight.hollight.int_sub_def"
488 "int_sgn_th" > "HOLLight.hollight.int_sgn_th"
489 "int_sgn_def" > "HOLLight.hollight.int_sgn_def"
490 "int_pow_th" > "HOLLight.hollight.int_pow_th"
491 "int_pow_def" > "HOLLight.hollight.int_pow_def"
492 "int_of_num_th" > "HOLLight.hollight.int_of_num_th"
493 "int_of_num_def" > "HOLLight.hollight.int_of_num_def"
494 "int_neg_th" > "HOLLight.hollight.int_neg_th"
495 "int_neg_def" > "HOLLight.hollight.int_neg_def"
496 "int_mul_th" > "HOLLight.hollight.int_mul_th"
497 "int_mul_def" > "HOLLight.hollight.int_mul_def"
498 "int_mod_def" > "HOLLight.hollight.int_mod_def"
499 "int_min_th" > "HOLLight.hollight.int_min_th"
500 "int_min_def" > "HOLLight.hollight.int_min_def"
501 "int_max_th" > "HOLLight.hollight.int_max_th"
502 "int_max_def" > "HOLLight.hollight.int_max_def"
503 "int_lt_def" > "HOLLight.hollight.int_lt_def"
504 "int_le_def" > "HOLLight.hollight.int_le_def"
505 "int_gt_def" > "HOLLight.hollight.int_gt_def"
506 "int_ge_def" > "HOLLight.hollight.int_ge_def"
507 "int_gcd_def" > "HOLLight.hollight.int_gcd_def"
508 "int_eq" > "HOLLight.hollight.int.real_of_int_inject"
509 "int_divides_def" > "HOLLight.hollight.int_divides_def"
510 "int_coprime_def" > "HOLLight.hollight.int_coprime_def"
511 "int_congruent" > "HOLLight.hollight.int_congruent"
512 "int_add_th" > "HOLLight.hollight.int_add_th"
513 "int_add_def" > "HOLLight.hollight.int_add_def"
514 "int_abs_th" > "HOLLight.hollight.int_abs_th"
515 "int_abs_def" > "HOLLight.hollight.int_abs_def"
516 "hreal_of_num_def" > "HOLLight.hollight.hreal_of_num_def"
517 "hreal_mul_def" > "HOLLight.hollight.hreal_mul_def"
518 "hreal_le_def" > "HOLLight.hollight.hreal_le_def"
519 "hreal_inv_def" > "HOLLight.hollight.hreal_inv_def"
520 "hreal_add_def" > "HOLLight.hollight.hreal_add_def"
521 "fstcart_def" > "HOLLight.hollight.fstcart_def"
522 "eqeq_def" > "HOLLight.hollight.eqeq_def"
523 "elemma0" > "HOLLight.hollight.elemma0"
524 "div_def" > "HOLLight.hollight.div_def"
525 "dist_def" > "HOLLight.hollight.dist_def"
526 "dimindex_def" > "HOLLight.hollight.dimindex_def"
527 "dest_int_rep" > "HOLLight.hollight.dest_int_rep"
528 "cth" > "HOLLight.hollight.cth"
529 "bool_RECURSION" > "HOLLight.hollight.bool_RECURSION"
530 "bool_INDUCT" > "Product_Type.bool.induct"
531 "ax__3" > "HOL4Setup.INFINITY_AX"
532 "ax__2" > "Hilbert_Choice.someI"
533 "ax__1" > "HOL.eta_contract_eq"
534 "admissible_def" > "HOLLight.hollight.admissible_def"
535 "_UNGUARDED_PATTERN_def" > "HOLLight.hollight._UNGUARDED_PATTERN_def"
536 "_SEQPATTERN_def" > "HOLLight.hollight._SEQPATTERN_def"
537 "_MATCH_def" > "HOLLight.hollight._MATCH_def"
538 "_GUARDED_PATTERN_def" > "HOLLight.hollight._GUARDED_PATTERN_def"
539 "_FUNCTION_def" > "HOLLight.hollight._FUNCTION_def"
540 "_FALSITY__def" > "HOLLight.hollight._FALSITY__def"
541 "_11937_def" > "HOLLight.hollight._11937_def"
542 "ZRECSPACE_def" > "HOLLight.hollight.ZRECSPACE_def"
543 "ZIP" > "HOLLightList.ZIP"
544 "ZCONSTR_def" > "HOLLight.hollight.ZCONSTR_def"
545 "ZCONSTR_ZBOT" > "HOLLight.hollight.ZCONSTR_ZBOT"
546 "ZBOT_def" > "HOLLight.hollight.ZBOT_def"
547 "WLOG_LT" > "HOLLight.hollight.WLOG_LT"
548 "WLOG_LE" > "HOLLight.hollight.WLOG_LE"
549 "WF_num" > "HOLLight.hollight.WF_num"
550 "WF_UREC_WF" > "HOLLight.hollight.WF_UREC_WF"
551 "WF_UREC" > "HOLLight.hollight.WF_UREC"
552 "WF_SUBSET" > "HOLLight.hollight.WF_SUBSET"
553 "WF_REFL" > "HOLLight.hollight.WF_REFL"
554 "WF_REC_num" > "HOLLight.hollight.WF_REC_num"
555 "WF_REC_WF" > "HOLLight.hollight.WF_REC_WF"
556 "WF_REC_TAIL_GENERAL" > "HOLLight.hollight.WF_REC_TAIL_GENERAL"
557 "WF_REC_TAIL" > "HOLLight.hollight.WF_REC_TAIL"
558 "WF_REC_INVARIANT" > "HOLLight.hollight.WF_REC_INVARIANT"
559 "WF_REC" > "HOLLight.hollight.WF_REC"
560 "WF_POINTWISE" > "HOLLight.hollight.WF_POINTWISE"
561 "WF_MEASURE_GEN" > "HOLLight.hollight.WF_MEASURE_GEN"
562 "WF_MEASURE" > "HOLLight.hollight.WF_MEASURE"
563 "WF_LEX_DEPENDENT" > "HOLLight.hollight.WF_LEX_DEPENDENT"
564 "WF_LEX" > "HOLLight.hollight.WF_LEX"
565 "WF_INT_MEASURE_2" > "HOLLight.hollight.WF_INT_MEASURE_2"
566 "WF_INT_MEASURE" > "HOLLight.hollight.WF_INT_MEASURE"
567 "WF_IND" > "HOLLight.hollight.WF_IND"
568 "WF_FINITE" > "HOLLight.hollight.WF_FINITE"
569 "WF_FALSE" > "Wellfounded.wfP_empty"
570 "WF_EREC" > "HOLLight.hollight.WF_EREC"
571 "WF_EQ" > "HOLLight.hollight.WF_EQ"
572 "WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
573 "UNWIND_THM2" > "HOL.simp_thms_39"
574 "UNWIND_THM1" > "HOL.simp_thms_40"
575 "UNIV_SUBSET" > "Orderings.top_class.top_unique"
576 "UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
577 "UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
578 "UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
579 "UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
580 "UNION_SUBSET" > "Lattices.semilattice_sup_class.le_sup_iff"
581 "UNION_OVER_INTER" > "Lattices.distrib_lattice_class.distrib_3"
582 "UNION_IDEMPOT" > "Big_Operators.lattice_class.Sup_fin.idem"
583 "UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
584 "UNION_COMM" > "Lattices.lattice_class.inf_sup_aci_5"
585 "UNION_ASSOC" > "Lattices.lattice_class.inf_sup_aci_6"
586 "UNION_ACI" > "HOLLight.hollight.UNION_ACI"
587 "UNIONS_UNION" > "Complete_Lattices.Union_Un_distrib"
588 "UNIONS_SUBSET" > "HOLLight.hollight.UNIONS_SUBSET"
589 "UNIONS_INTERS" > "HOLLight.hollight.UNIONS_INTERS"
590 "UNIONS_INSERT" > "Complete_Lattices.Union_insert"
591 "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
592 "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
593 "UNIONS_2" > "Complete_Lattices.Un_eq_Union"
594 "UNIONS_1" > "Complete_Lattices.complete_lattice_class.Sup_singleton"
595 "UNIONS_0" > "Complete_Lattices.Union_empty"
596 "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
597 "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
598 "TYDEF_real" > "HOLLight.hollight.TYDEF_real"
599 "TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"
600 "TYDEF_int" > "HOLLight.hollight.TYDEF_int"
601 "TYDEF_hreal" > "HOLLight.hollight.TYDEF_hreal"
602 "TYDEF_finite_sum" > "HOLLight.hollight.TYDEF_finite_sum"
603 "TYDEF_finite_image" > "HOLLight.hollight.TYDEF_finite_image"
604 "TYDEF_char" > "HOLLight.hollight.TYDEF_char"
605 "TYDEF_cart" > "HOLLight.hollight.TYDEF_cart"
606 "TYDEF_3" > "HOLLight.hollight.TYDEF_3"
607 "TYDEF_2" > "HOLLight.hollight.TYDEF_2"
608 "TWO" > "HOLLight.hollight.TWO"
609 "TRIV_OR_FORALL_THM" > "HOLLight.hollight.TRIV_OR_FORALL_THM"
610 "TRIV_FORALL_OR_THM" > "HOLLight.hollight.TRIV_FORALL_OR_THM"
611 "TRIV_FORALL_IMP_THM" > "HOLLight.hollight.TRIV_FORALL_IMP_THM"
612 "TRIV_EXISTS_IMP_THM" > "HOLLight.hollight.TRIV_EXISTS_IMP_THM"
613 "TRIV_EXISTS_AND_THM" > "HOLLight.hollight.TRIV_EXISTS_AND_THM"
614 "TRIV_AND_EXISTS_THM" > "HOLLight.hollight.TRIV_AND_EXISTS_THM"
615 "TREAL_OF_NUM_WELLDEF" > "HOLLight.hollight.TREAL_OF_NUM_WELLDEF"
616 "TREAL_OF_NUM_MUL" > "HOLLight.hollight.TREAL_OF_NUM_MUL"
617 "TREAL_OF_NUM_LE" > "HOLLight.hollight.TREAL_OF_NUM_LE"
618 "TREAL_OF_NUM_EQ" > "HOLLight.hollight.TREAL_OF_NUM_EQ"
619 "TREAL_OF_NUM_ADD" > "HOLLight.hollight.TREAL_OF_NUM_ADD"
620 "TREAL_NEG_WELLDEF" > "HOLLight.hollight.TREAL_NEG_WELLDEF"
621 "TREAL_MUL_WELLDEFR" > "HOLLight.hollight.TREAL_MUL_WELLDEFR"
622 "TREAL_MUL_WELLDEF" > "HOLLight.hollight.TREAL_MUL_WELLDEF"
623 "TREAL_MUL_SYM_EQ" > "HOLLight.hollight.TREAL_MUL_SYM_EQ"
624 "TREAL_MUL_SYM" > "HOLLight.hollight.TREAL_MUL_SYM"
625 "TREAL_MUL_LINV" > "HOLLight.hollight.TREAL_MUL_LINV"
626 "TREAL_MUL_LID" > "HOLLight.hollight.TREAL_MUL_LID"
627 "TREAL_MUL_ASSOC" > "HOLLight.hollight.TREAL_MUL_ASSOC"
628 "TREAL_LE_WELLDEF" > "HOLLight.hollight.TREAL_LE_WELLDEF"
629 "TREAL_LE_TRANS" > "HOLLight.hollight.TREAL_LE_TRANS"
630 "TREAL_LE_TOTAL" > "HOLLight.hollight.TREAL_LE_TOTAL"
631 "TREAL_LE_REFL" > "HOLLight.hollight.TREAL_LE_REFL"
632 "TREAL_LE_MUL" > "HOLLight.hollight.TREAL_LE_MUL"
633 "TREAL_LE_LADD_IMP" > "HOLLight.hollight.TREAL_LE_LADD_IMP"
634 "TREAL_LE_ANTISYM" > "HOLLight.hollight.TREAL_LE_ANTISYM"
635 "TREAL_INV_WELLDEF" > "HOLLight.hollight.TREAL_INV_WELLDEF"
636 "TREAL_INV_0" > "HOLLight.hollight.TREAL_INV_0"
637 "TREAL_EQ_TRANS" > "HOLLight.hollight.TREAL_EQ_TRANS"
638 "TREAL_EQ_SYM" > "HOLLight.hollight.TREAL_EQ_SYM"
639 "TREAL_EQ_REFL" > "HOLLight.hollight.TREAL_EQ_REFL"
640 "TREAL_EQ_IMP_LE" > "HOLLight.hollight.TREAL_EQ_IMP_LE"
641 "TREAL_EQ_AP" > "HOLLight.hollight.TREAL_EQ_AP"
642 "TREAL_ADD_WELLDEFR" > "HOLLight.hollight.TREAL_ADD_WELLDEFR"
643 "TREAL_ADD_WELLDEF" > "HOLLight.hollight.TREAL_ADD_WELLDEF"
644 "TREAL_ADD_SYM_EQ" > "HOLLight.hollight.TREAL_ADD_SYM_EQ"
645 "TREAL_ADD_SYM" > "HOLLight.hollight.TREAL_ADD_SYM"
646 "TREAL_ADD_LINV" > "HOLLight.hollight.TREAL_ADD_LINV"
647 "TREAL_ADD_LID" > "HOLLight.hollight.TREAL_ADD_LID"
648 "TREAL_ADD_LDISTRIB" > "HOLLight.hollight.TREAL_ADD_LDISTRIB"
649 "TREAL_ADD_ASSOC" > "HOLLight.hollight.TREAL_ADD_ASSOC"
650 "TRANSITIVE_STEPWISE_LT_EQ" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LT_EQ"
651 "TRANSITIVE_STEPWISE_LT" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LT"
652 "TRANSITIVE_STEPWISE_LE_EQ" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LE_EQ"
653 "TRANSITIVE_STEPWISE_LE" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LE"
654 "TOPOLOGICAL_SORT" > "HOLLight.hollight.TOPOLOGICAL_SORT"
655 "SWAP_FORALL_THM" > "HOL.all_comm"
656 "SWAP_EXISTS_THM" > "HOL.ex_comm"
657 "SURJ_def" > "HOLLight.hollight.SURJ_def"
658 "SURJECTIVE_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_RIGHT_INVERSE"
659 "SURJECTIVE_ON_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_ON_RIGHT_INVERSE"
660 "SURJECTIVE_ON_IMAGE" > "HOLLight.hollight.SURJECTIVE_ON_IMAGE"
661 "SURJECTIVE_MAP" > "HOLLightList.SURJECTIVE_MAP"
662 "SURJECTIVE_IMAGE_THM" > "HOLLight.hollight.SURJECTIVE_IMAGE_THM"
663 "SURJECTIVE_IMAGE_EQ" > "HOLLight.hollight.SURJECTIVE_IMAGE_EQ"
664 "SURJECTIVE_IMAGE" > "HOLLight.hollight.SURJECTIVE_IMAGE"
665 "SURJECTIVE_IFF_INJECTIVE_GEN" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE_GEN"
666 "SURJECTIVE_IFF_INJECTIVE" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE"
667 "SURJECTIVE_FORALL_THM" > "HOLLight.hollight.SURJECTIVE_FORALL_THM"
668 "SURJECTIVE_EXISTS_THM" > "HOLLight.hollight.SURJECTIVE_EXISTS_THM"
669 "SUPPORT_SUPPORT" > "HOLLight.hollight.SUPPORT_SUPPORT"
670 "SUPPORT_SUBSET" > "HOLLight.hollight.SUPPORT_SUBSET"
671 "SUPPORT_EMPTY" > "HOLLight.hollight.SUPPORT_EMPTY"
672 "SUPPORT_DELTA" > "HOLLight.hollight.SUPPORT_DELTA"
673 "SUPPORT_CLAUSES" > "HOLLight.hollight.SUPPORT_CLAUSES"
674 "SUPERADMISSIBLE_TAIL" > "HOLLight.hollight.SUPERADMISSIBLE_TAIL"
675 "SUPERADMISSIBLE_T" > "HOLLight.hollight.SUPERADMISSIBLE_T"
676 "SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN"
677 "SUPERADMISSIBLE_MATCH_SEQPATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_SEQPATTERN"
678 "SUPERADMISSIBLE_MATCH_GUARDED_PATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_GUARDED_PATTERN"
679 "SUPERADMISSIBLE_CONST" > "HOLLight.hollight.SUPERADMISSIBLE_CONST"
680 "SUPERADMISSIBLE_COND" > "HOLLight.hollight.SUPERADMISSIBLE_COND"
681 "SUM_ZERO_EXISTS" > "HOLLight.hollight.SUM_ZERO_EXISTS"
682 "SUM_UNION_RZERO" > "HOLLight.hollight.SUM_UNION_RZERO"
683 "SUM_UNION_NONZERO" > "HOLLight.hollight.SUM_UNION_NONZERO"
684 "SUM_UNION_LZERO" > "HOLLight.hollight.SUM_UNION_LZERO"
685 "SUM_UNION_EQ" > "HOLLight.hollight.SUM_UNION_EQ"
686 "SUM_UNIONS_NONZERO" > "HOLLight.hollight.SUM_UNIONS_NONZERO"
687 "SUM_UNION" > "HOLLight.hollight.SUM_UNION"
688 "SUM_TRIV_NUMSEG" > "HOLLight.hollight.SUM_TRIV_NUMSEG"
689 "SUM_SWAP_NUMSEG" > "HOLLight.hollight.SUM_SWAP_NUMSEG"
690 "SUM_SWAP" > "HOLLight.hollight.SUM_SWAP"
691 "SUM_SUPPORT" > "HOLLight.hollight.SUM_SUPPORT"
692 "SUM_SUPERSET" > "HOLLight.hollight.SUM_SUPERSET"
693 "SUM_SUM_RESTRICT" > "HOLLight.hollight.SUM_SUM_RESTRICT"
694 "SUM_SUM_PRODUCT" > "HOLLight.hollight.SUM_SUM_PRODUCT"
695 "SUM_SUB_NUMSEG" > "HOLLight.hollight.SUM_SUB_NUMSEG"
696 "SUM_SUBSET_SIMPLE" > "HOLLight.hollight.SUM_SUBSET_SIMPLE"
697 "SUM_SUBSET" > "HOLLight.hollight.SUM_SUBSET"
698 "SUM_SUB" > "HOLLight.hollight.SUM_SUB"
699 "SUM_SING_NUMSEG" > "HOLLight.hollight.SUM_SING_NUMSEG"
700 "SUM_SING" > "HOLLight.hollight.SUM_SING"
701 "SUM_RMUL" > "HOLLight.hollight.SUM_RMUL"
702 "SUM_RESTRICT_SET" > "HOLLight.hollight.SUM_RESTRICT_SET"
703 "SUM_RESTRICT" > "HOLLight.hollight.SUM_RESTRICT"
704 "SUM_POS_LE_NUMSEG" > "HOLLight.hollight.SUM_POS_LE_NUMSEG"
705 "SUM_POS_LE" > "HOLLight.hollight.SUM_POS_LE"
706 "SUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_POS_EQ_0_NUMSEG"
707 "SUM_POS_EQ_0" > "HOLLight.hollight.SUM_POS_EQ_0"
708 "SUM_POS_BOUND" > "HOLLight.hollight.SUM_POS_BOUND"
709 "SUM_PARTIAL_SUC" > "HOLLight.hollight.SUM_PARTIAL_SUC"
710 "SUM_PARTIAL_PRE" > "HOLLight.hollight.SUM_PARTIAL_PRE"
711 "SUM_PAIR" > "HOLLight.hollight.SUM_PAIR"
712 "SUM_OFFSET_0" > "HOLLight.hollight.SUM_OFFSET_0"
713 "SUM_OFFSET" > "HOLLight.hollight.SUM_OFFSET"
714 "SUM_NEG" > "HOLLight.hollight.SUM_NEG"
715 "SUM_MULTICOUNT_GEN" > "HOLLight.hollight.SUM_MULTICOUNT_GEN"
716 "SUM_MULTICOUNT" > "HOLLight.hollight.SUM_MULTICOUNT"
717 "SUM_LT_ALL" > "HOLLight.hollight.SUM_LT_ALL"
718 "SUM_LT" > "HOLLight.hollight.SUM_LT"
719 "SUM_LMUL" > "HOLLight.hollight.SUM_LMUL"
720 "SUM_LE_NUMSEG" > "HOLLight.hollight.SUM_LE_NUMSEG"
721 "SUM_LE_INCLUDED" > "HOLLight.hollight.SUM_LE_INCLUDED"
722 "SUM_LE" > "HOLLight.hollight.SUM_LE"
723 "SUM_INJECTION" > "HOLLight.hollight.SUM_INJECTION"
724 "SUM_INCL_EXCL" > "HOLLight.hollight.SUM_INCL_EXCL"
725 "SUM_IMAGE_NONZERO" > "HOLLight.hollight.SUM_IMAGE_NONZERO"
726 "SUM_IMAGE_LE" > "HOLLight.hollight.SUM_IMAGE_LE"
727 "SUM_IMAGE_GEN" > "HOLLight.hollight.SUM_IMAGE_GEN"
728 "SUM_IMAGE" > "HOLLight.hollight.SUM_IMAGE"
729 "SUM_GROUP" > "HOLLight.hollight.SUM_GROUP"
730 "SUM_EQ_SUPERSET" > "HOLLight.hollight.SUM_EQ_SUPERSET"
731 "SUM_EQ_NUMSEG" > "HOLLight.hollight.SUM_EQ_NUMSEG"
732 "SUM_EQ_GENERAL_INVERSES" > "HOLLight.hollight.SUM_EQ_GENERAL_INVERSES"
733 "SUM_EQ_GENERAL" > "HOLLight.hollight.SUM_EQ_GENERAL"
734 "SUM_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_EQ_0_NUMSEG"
735 "SUM_EQ_0" > "HOLLight.hollight.SUM_EQ_0"
736 "SUM_EQ" > "HOLLight.hollight.SUM_EQ"
737 "SUM_DIFFS_ALT" > "HOLLight.hollight.SUM_DIFFS_ALT"
738 "SUM_DIFFS" > "HOLLight.hollight.SUM_DIFFS"
739 "SUM_DIFF" > "HOLLight.hollight.SUM_DIFF"
740 "SUM_DELTA" > "HOLLight.hollight.SUM_DELTA"
741 "SUM_DELETE_CASES" > "HOLLight.hollight.SUM_DELETE_CASES"
742 "SUM_DELETE" > "HOLLight.hollight.SUM_DELETE"
743 "SUM_CONST_NUMSEG" > "HOLLight.hollight.SUM_CONST_NUMSEG"
744 "SUM_CONST" > "HOLLight.hollight.SUM_CONST"
745 "SUM_COMBINE_R" > "HOLLight.hollight.SUM_COMBINE_R"
746 "SUM_COMBINE_L" > "HOLLight.hollight.SUM_COMBINE_L"
747 "SUM_CLOSED" > "HOLLight.hollight.SUM_CLOSED"
748 "SUM_CLAUSES_RIGHT" > "HOLLight.hollight.SUM_CLAUSES_RIGHT"
749 "SUM_CLAUSES_NUMSEG" > "HOLLight.hollight.SUM_CLAUSES_NUMSEG"
750 "SUM_CLAUSES_LEFT" > "HOLLight.hollight.SUM_CLAUSES_LEFT"
751 "SUM_CLAUSES" > "HOLLight.hollight.SUM_CLAUSES"
752 "SUM_CASES_1" > "HOLLight.hollight.SUM_CASES_1"
753 "SUM_CASES" > "HOLLight.hollight.SUM_CASES"
754 "SUM_BOUND_LT_GEN" > "HOLLight.hollight.SUM_BOUND_LT_GEN"
755 "SUM_BOUND_LT_ALL" > "HOLLight.hollight.SUM_BOUND_LT_ALL"
756 "SUM_BOUND_LT" > "HOLLight.hollight.SUM_BOUND_LT"
757 "SUM_BOUND_GEN" > "HOLLight.hollight.SUM_BOUND_GEN"
758 "SUM_BOUND" > "HOLLight.hollight.SUM_BOUND"
759 "SUM_BIJECTION" > "HOLLight.hollight.SUM_BIJECTION"
760 "SUM_ADD_SPLIT" > "HOLLight.hollight.SUM_ADD_SPLIT"
761 "SUM_ADD_NUMSEG" > "HOLLight.hollight.SUM_ADD_NUMSEG"
762 "SUM_ADD_GEN" > "HOLLight.hollight.SUM_ADD_GEN"
763 "SUM_ADD" > "HOLLight.hollight.SUM_ADD"
764 "SUM_ABS_NUMSEG" > "HOLLight.hollight.SUM_ABS_NUMSEG"
765 "SUM_ABS_LE" > "HOLLight.hollight.SUM_ABS_LE"
766 "SUM_ABS_BOUND" > "HOLLight.hollight.SUM_ABS_BOUND"
767 "SUM_ABS" > "HOLLight.hollight.SUM_ABS"
768 "SUM_0" > "HOLLight.hollight.SUM_0"
769 "SUC_SUB1" > "Nat.diff_Suc_1"
770 "SUC_INJ" > "HOLLightCompat.SUC_INJ"
771 "SUB_SUC" > "Nat.diff_Suc_Suc"
772 "SUB_REFL" > "Nat.diff_self_eq_0"
773 "SUB_PRESUC" > "HOLLight.hollight.SUB_PRESUC"
774 "SUB_EQ_0" > "Nat.diff_is_0_eq"
775 "SUB_ELIM_THM" > "HOLLight.hollight.SUB_ELIM_THM"
776 "SUB_ADD_RCANCEL" > "Nat.diff_cancel2"
777 "SUB_ADD_LCANCEL" > "Nat.diff_cancel"
778 "SUB_ADD" > "Nat.le_add_diff_inverse2"
779 "SUB_0" > "HOLLight.hollight.SUB_0"
780 "SUBSET_UNIV" > "Orderings.top_class.top_greatest"
781 "SUBSET_UNION_ABSORPTION" > "Lattices.semilattice_sup_class.le_iff_sup"
782 "SUBSET_UNIONS" > "Complete_Lattices.Union_mono"
783 "SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
784 "SUBSET_TRANS" > "Orderings.order_trans_rules_23"
785 "SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
786 "SUBSET_REFL" > "Inductive.basic_monos_1"
787 "SUBSET_PSUBSET_TRANS" > "Orderings.order_le_less_trans"
788 "SUBSET_NUMSEG" > "HOLLight.hollight.SUBSET_NUMSEG"
789 "SUBSET_INTER_ABSORPTION" > "Lattices.semilattice_inf_class.le_iff_inf"
790 "SUBSET_INTER" > "Lattices.semilattice_inf_class.le_inf_iff"
791 "SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
792 "SUBSET_INSERT" > "Set.subset_insert"
793 "SUBSET_IMAGE" > "Set.subset_image_iff"
794 "SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
795 "SUBSET_DIFF" > "Set.Diff_subset"
796 "SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
797 "SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
798 "SUBSET_ANTISYM_EQ" > "Orderings.order_class.eq_iff"
799 "SUBSET_ANTISYM" > "Orderings.order_antisym"
800 "SND" > "Product_Type.snd_conv"
801 "SKOLEM_THM" > "HOLLight.hollight.SKOLEM_THM"
802 "SING_def" > "HOLLight.hollight.SING_def"
803 "SING_SUBSET" > "HOLLight.hollight.SING_SUBSET"
804 "SING_GSPEC" > "HOLLight.hollight.SING_GSPEC"
805 "SIMPLE_IMAGE_GEN" > "HOLLight.hollight.SIMPLE_IMAGE_GEN"
806 "SIMPLE_IMAGE" > "HOLLight.hollight.SIMPLE_IMAGE"
807 "SET_RECURSION_LEMMA" > "HOLLight.hollight.SET_RECURSION_LEMMA"
808 "SET_PROVE_CASES" > "HOLLight.hollight.SET_PROVE_CASES"
809 "SET_PAIR_THM" > "HOLLight.hollight.SET_PAIR_THM"
810 "SET_OF_LIST_MAP" > "List.set_map"
811 "SET_OF_LIST_EQ_EMPTY" > "List.set_empty"
812 "SET_OF_LIST_APPEND" > "List.set_append"
813 "SET_CASES" > "HOLLight.hollight.SET_CASES"
814 "SEMIRING_PTHS" > "HOLLight.hollight.SEMIRING_PTHS"
815 "SELECT_UNIQUE" > "HOLLight.hollight.SELECT_UNIQUE"
816 "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
817 "SELECT_LEMMA" > "Hilbert_Choice.some_sym_eq_trivial"
818 "RIGHT_SUB_DISTRIB" > "Nat.diff_mult_distrib"
819 "RIGHT_OR_FORALL_THM" > "HOL.all_simps_4"
820 "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
821 "RIGHT_OR_DISTRIB" > "Groebner_Basis.dnf_2"
822 "RIGHT_IMP_FORALL_THM" > "HOL.all_simps_6"
823 "RIGHT_IMP_EXISTS_THM" > "HOL.ex_simps_6"
824 "RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
825 "RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
826 "RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
827 "RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
828 "RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
829 "RIGHT_AND_EXISTS_THM" > "HOL.ex_simps_2"
830 "RIGHT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_26"
831 "REVERSE_REVERSE" > "List.rev_rev_ident"
832 "REVERSE_APPEND" > "List.rev_append"
833 "REST_def" > "HOLLight.hollight.REST_def"
834 "REFL_CLAUSE" > "Groebner_Basis.bool_simps_6"
835 "REAL_WLOG_LT" > "HOLLight.hollight.REAL_WLOG_LT"
836 "REAL_WLOG_LE" > "HOLLight.hollight.REAL_WLOG_LE"
837 "REAL_SUB_TRIANGLE" > "HOLLight.hollight.REAL_SUB_TRIANGLE"
838 "REAL_SUB_SUB2" > "HOLLight.hollight.REAL_SUB_SUB2"
839 "REAL_SUB_SUB" > "HOLLight.hollight.REAL_SUB_SUB"
840 "REAL_SUB_RZERO" > "HOLLight.hollight.REAL_SUB_RZERO"
841 "REAL_SUB_RNEG" > "HOLLight.hollight.REAL_SUB_RNEG"
842 "REAL_SUB_REFL" > "HOLLight.hollight.REAL_SUB_REFL"
843 "REAL_SUB_RDISTRIB" > "HOLLight.hollight.REAL_SUB_RDISTRIB"
844 "REAL_SUB_POW_R1" > "HOLLight.hollight.REAL_SUB_POW_R1"
845 "REAL_SUB_POW_L1" > "HOLLight.hollight.REAL_SUB_POW_L1"
846 "REAL_SUB_POW" > "HOLLight.hollight.REAL_SUB_POW"
847 "REAL_SUB_NEG2" > "HOLLight.hollight.REAL_SUB_NEG2"
848 "REAL_SUB_LZERO" > "HOLLight.hollight.REAL_SUB_LZERO"
849 "REAL_SUB_LT" > "HOLLight.hollight.REAL_SUB_LT"
850 "REAL_SUB_LNEG" > "HOLLight.hollight.REAL_SUB_LNEG"
851 "REAL_SUB_LE" > "HOLLight.hollight.REAL_SUB_LE"
852 "REAL_SUB_LDISTRIB" > "HOLLight.hollight.REAL_SUB_LDISTRIB"
853 "REAL_SUB_INV" > "HOLLight.hollight.REAL_SUB_INV"
854 "REAL_SUB_ADD2" > "HOLLight.hollight.REAL_SUB_ADD2"
855 "REAL_SUB_ADD" > "HOLLight.hollight.REAL_SUB_ADD"
856 "REAL_SUB_ABS" > "HOLLight.hollight.REAL_SUB_ABS"
857 "REAL_SUB_0" > "HOLLight.hollight.REAL_SUB_0"
858 "REAL_SOS_EQ_0" > "HOLLight.hollight.REAL_SOS_EQ_0"
859 "REAL_SGN_NEG" > "HOLLight.hollight.REAL_SGN_NEG"
860 "REAL_SGN_MUL" > "HOLLight.hollight.REAL_SGN_MUL"
861 "REAL_SGN_INV" > "HOLLight.hollight.REAL_SGN_INV"
862 "REAL_SGN_DIV" > "HOLLight.hollight.REAL_SGN_DIV"
863 "REAL_SGN_ABS" > "HOLLight.hollight.REAL_SGN_ABS"
864 "REAL_SGN_0" > "HOLLight.hollight.REAL_SGN_0"
865 "REAL_SGN" > "HOLLight.hollight.REAL_SGN"
866 "REAL_RNEG_UNIQ" > "HOLLight.hollight.REAL_RNEG_UNIQ"
867 "REAL_POW_ZERO" > "HOLLight.hollight.REAL_POW_ZERO"
868 "REAL_POW_SUB" > "HOLLight.hollight.REAL_POW_SUB"
869 "REAL_POW_POW" > "HOLLight.hollight.REAL_POW_POW"
870 "REAL_POW_ONE" > "HOLLight.hollight.REAL_POW_ONE"
871 "REAL_POW_NZ" > "HOLLight.hollight.REAL_POW_NZ"
872 "REAL_POW_NEG" > "HOLLight.hollight.REAL_POW_NEG"
873 "REAL_POW_MUL" > "HOLLight.hollight.REAL_POW_MUL"
874 "REAL_POW_MONO_LT" > "HOLLight.hollight.REAL_POW_MONO_LT"
875 "REAL_POW_MONO_INV" > "HOLLight.hollight.REAL_POW_MONO_INV"
876 "REAL_POW_MONO" > "HOLLight.hollight.REAL_POW_MONO"
877 "REAL_POW_LT_1" > "HOLLight.hollight.REAL_POW_LT_1"
878 "REAL_POW_LT2_REV" > "HOLLight.hollight.REAL_POW_LT2_REV"
879 "REAL_POW_LT2_ODD_EQ" > "HOLLight.hollight.REAL_POW_LT2_ODD_EQ"
880 "REAL_POW_LT2_ODD" > "HOLLight.hollight.REAL_POW_LT2_ODD"
881 "REAL_POW_LT2" > "HOLLight.hollight.REAL_POW_LT2"
882 "REAL_POW_LT" > "HOLLight.hollight.REAL_POW_LT"
883 "REAL_POW_LE_1" > "HOLLight.hollight.REAL_POW_LE_1"
884 "REAL_POW_LE2_REV" > "HOLLight.hollight.REAL_POW_LE2_REV"
885 "REAL_POW_LE2_ODD_EQ" > "HOLLight.hollight.REAL_POW_LE2_ODD_EQ"
886 "REAL_POW_LE2_ODD" > "HOLLight.hollight.REAL_POW_LE2_ODD"
887 "REAL_POW_LE2" > "HOLLight.hollight.REAL_POW_LE2"
888 "REAL_POW_LE" > "HOLLight.hollight.REAL_POW_LE"
889 "REAL_POW_INV" > "HOLLight.hollight.REAL_POW_INV"
890 "REAL_POW_EQ_ODD_EQ" > "HOLLight.hollight.REAL_POW_EQ_ODD_EQ"
891 "REAL_POW_EQ_ODD" > "HOLLight.hollight.REAL_POW_EQ_ODD"
892 "REAL_POW_EQ_EQ" > "HOLLight.hollight.REAL_POW_EQ_EQ"
893 "REAL_POW_EQ_ABS" > "HOLLight.hollight.REAL_POW_EQ_ABS"
894 "REAL_POW_EQ_1_IMP" > "HOLLight.hollight.REAL_POW_EQ_1_IMP"
895 "REAL_POW_EQ_1" > "HOLLight.hollight.REAL_POW_EQ_1"
896 "REAL_POW_EQ_0" > "HOLLight.hollight.REAL_POW_EQ_0"
897 "REAL_POW_EQ" > "HOLLight.hollight.REAL_POW_EQ"
898 "REAL_POW_DIV" > "HOLLight.hollight.REAL_POW_DIV"
899 "REAL_POW_ADD" > "HOLLight.hollight.REAL_POW_ADD"
900 "REAL_POW_2" > "HOLLight.hollight.REAL_POW_2"
901 "REAL_POW_1_LT" > "HOLLight.hollight.REAL_POW_1_LT"
902 "REAL_POW_1_LE" > "HOLLight.hollight.REAL_POW_1_LE"
903 "REAL_POW_1" > "HOLLight.hollight.REAL_POW_1"
904 "REAL_POW2_ABS" > "HOLLight.hollight.REAL_POW2_ABS"
905 "REAL_POS_NZ" > "HOLLight.hollight.REAL_POS_NZ"
906 "REAL_POS" > "HOLLight.hollight.REAL_POS"
907 "REAL_POLY_NEG_CLAUSES" > "HOLLight.hollight.REAL_POLY_NEG_CLAUSES"
908 "REAL_POLY_CLAUSES" > "HOLLight.hollight.REAL_POLY_CLAUSES"
909 "REAL_OF_NUM_SUM_NUMSEG" > "HOLLight.hollight.REAL_OF_NUM_SUM_NUMSEG"
910 "REAL_OF_NUM_SUM" > "HOLLight.hollight.REAL_OF_NUM_SUM"
911 "REAL_OF_NUM_SUC" > "HOLLight.hollight.REAL_OF_NUM_SUC"
912 "REAL_OF_NUM_SUB" > "HOLLight.hollight.REAL_OF_NUM_SUB"
913 "REAL_OF_NUM_POW" > "HOLLight.hollight.REAL_OF_NUM_POW"
914 "REAL_OF_NUM_MIN" > "HOLLight.hollight.REAL_OF_NUM_MIN"
915 "REAL_OF_NUM_MAX" > "HOLLight.hollight.REAL_OF_NUM_MAX"
916 "REAL_OF_NUM_LT" > "HOLLight.hollight.REAL_OF_NUM_LT"
917 "REAL_OF_NUM_GT" > "HOLLight.hollight.REAL_OF_NUM_GT"
918 "REAL_OF_NUM_GE" > "HOLLight.hollight.REAL_OF_NUM_GE"
919 "REAL_NOT_LT" > "HOLLight.hollight.REAL_NOT_LT"
920 "REAL_NOT_LE" > "HOLLight.hollight.real_lt_def"
921 "REAL_NOT_EQ" > "HOLLight.hollight.REAL_NOT_EQ"
922 "REAL_NEG_SUB" > "HOLLight.hollight.REAL_NEG_SUB"
923 "REAL_NEG_RMUL" > "HOLLight.hollight.REAL_NEG_RMUL"
924 "REAL_NEG_NEG" > "HOLLight.hollight.REAL_NEG_NEG"
925 "REAL_NEG_MUL2" > "HOLLight.hollight.REAL_NEG_MUL2"
926 "REAL_NEG_MINUS1" > "HOLLight.hollight.REAL_NEG_MINUS1"
927 "REAL_NEG_LT0" > "HOLLight.hollight.REAL_NEG_LT0"
928 "REAL_NEG_LMUL" > "HOLLight.hollight.REAL_NEG_LMUL"
929 "REAL_NEG_LE0" > "HOLLight.hollight.REAL_NEG_LE0"
930 "REAL_NEG_GT0" > "HOLLight.hollight.REAL_NEG_GT0"
931 "REAL_NEG_GE0" > "HOLLight.hollight.REAL_NEG_GE0"
932 "REAL_NEG_EQ_0" > "HOLLight.hollight.REAL_NEG_EQ_0"
933 "REAL_NEG_EQ" > "HOLLight.hollight.REAL_NEG_EQ"
934 "REAL_NEG_ADD" > "HOLLight.hollight.REAL_NEG_ADD"
935 "REAL_NEG_0" > "HOLLight.hollight.REAL_NEG_0"
936 "REAL_NEGNEG" > "HOLLight.hollight.REAL_NEGNEG"
937 "REAL_MUL_RZERO" > "HOLLight.hollight.REAL_MUL_RZERO"
938 "REAL_MUL_RNEG" > "HOLLight.hollight.REAL_MUL_RNEG"
939 "REAL_MUL_RINV_UNIQ" > "HOLLight.hollight.REAL_MUL_RINV_UNIQ"
940 "REAL_MUL_RINV" > "HOLLight.hollight.REAL_MUL_RINV"
941 "REAL_MUL_RID" > "HOLLight.hollight.REAL_MUL_RID"
942 "REAL_MUL_POS_LT" > "HOLLight.hollight.REAL_MUL_POS_LT"
943 "REAL_MUL_POS_LE" > "HOLLight.hollight.REAL_MUL_POS_LE"
944 "REAL_MUL_LZERO" > "HOLLight.hollight.REAL_MUL_LZERO"
945 "REAL_MUL_LNEG" > "HOLLight.hollight.REAL_MUL_LNEG"
946 "REAL_MUL_LINV_UNIQ" > "HOLLight.hollight.REAL_MUL_LINV_UNIQ"
947 "REAL_MUL_AC" > "HOLLight.hollight.REAL_MUL_AC"
948 "REAL_MUL_2" > "HOLLight.hollight.REAL_MUL_2"
949 "REAL_MIN_SYM" > "HOLLight.hollight.REAL_MIN_SYM"
950 "REAL_MIN_MIN" > "HOLLight.hollight.REAL_MIN_MIN"
951 "REAL_MIN_MAX" > "HOLLight.hollight.REAL_MIN_MAX"
952 "REAL_MIN_LT" > "HOLLight.hollight.REAL_MIN_LT"
953 "REAL_MIN_LE" > "HOLLight.hollight.REAL_MIN_LE"
954 "REAL_MIN_ASSOC" > "HOLLight.hollight.REAL_MIN_ASSOC"
955 "REAL_MIN_ACI" > "HOLLight.hollight.REAL_MIN_ACI"
956 "REAL_MAX_SYM" > "HOLLight.hollight.REAL_MAX_SYM"
957 "REAL_MAX_MIN" > "HOLLight.hollight.REAL_MAX_MIN"
958 "REAL_MAX_MAX" > "HOLLight.hollight.REAL_MAX_MAX"
959 "REAL_MAX_LT" > "HOLLight.hollight.REAL_MAX_LT"
960 "REAL_MAX_LE" > "HOLLight.hollight.REAL_MAX_LE"
961 "REAL_MAX_ASSOC" > "HOLLight.hollight.REAL_MAX_ASSOC"
962 "REAL_MAX_ACI" > "HOLLight.hollight.REAL_MAX_ACI"
963 "REAL_LT_TRANS" > "HOLLight.hollight.REAL_LT_TRANS"
964 "REAL_LT_TOTAL" > "HOLLight.hollight.REAL_LT_TOTAL"
965 "REAL_LT_SUB_RADD" > "HOLLight.hollight.REAL_LT_SUB_RADD"
966 "REAL_LT_SUB_LADD" > "HOLLight.hollight.REAL_LT_SUB_LADD"
967 "REAL_LT_SQUARE_ABS" > "HOLLight.hollight.REAL_LT_SQUARE_ABS"
968 "REAL_LT_SQUARE" > "HOLLight.hollight.REAL_LT_SQUARE"
969 "REAL_LT_RNEG" > "HOLLight.hollight.REAL_LT_RNEG"
970 "REAL_LT_RMUL_EQ" > "HOLLight.hollight.REAL_LT_RMUL_EQ"
971 "REAL_LT_RMUL" > "HOLLight.hollight.REAL_LT_RMUL"
972 "REAL_LT_RINV" > "HOLLight.hollight.REAL_LT_RINV"
973 "REAL_LT_REFL" > "HOLLight.hollight.REAL_LT_REFL"
974 "REAL_LT_RDIV_EQ" > "HOLLight.hollight.REAL_LT_RDIV_EQ"
975 "REAL_LT_RCANCEL_IMP" > "HOLLight.hollight.REAL_LT_RCANCEL_IMP"
976 "REAL_LT_RADD" > "HOLLight.hollight.REAL_LT_RADD"
977 "REAL_LT_POW2" > "HOLLight.hollight.REAL_LT_POW2"
978 "REAL_LT_NEGTOTAL" > "HOLLight.hollight.REAL_LT_NEGTOTAL"
979 "REAL_LT_NEG2" > "HOLLight.hollight.REAL_LT_NEG2"
980 "REAL_LT_NEG" > "HOLLight.hollight.REAL_LT_NEG"
981 "REAL_LT_MUL_EQ" > "HOLLight.hollight.REAL_LT_MUL_EQ"
982 "REAL_LT_MUL2" > "HOLLight.hollight.REAL_LT_MUL2"
983 "REAL_LT_MUL" > "HOLLight.hollight.REAL_LT_MUL"
984 "REAL_LT_MIN" > "HOLLight.hollight.REAL_LT_MIN"
985 "REAL_LT_MAX" > "HOLLight.hollight.REAL_LT_MAX"
986 "REAL_LT_LNEG" > "HOLLight.hollight.REAL_LT_LNEG"
987 "REAL_LT_LMUL_EQ" > "HOLLight.hollight.REAL_LT_LMUL_EQ"
988 "REAL_LT_LMUL" > "HOLLight.hollight.REAL_LT_LMUL"
989 "REAL_LT_LINV" > "HOLLight.hollight.REAL_LT_LINV"
990 "REAL_LT_LE" > "HOLLight.hollight.REAL_LT_LE"
991 "REAL_LT_LDIV_EQ" > "HOLLight.hollight.REAL_LT_LDIV_EQ"
992 "REAL_LT_LCANCEL_IMP" > "HOLLight.hollight.REAL_LT_LCANCEL_IMP"
993 "REAL_LT_LADD_IMP" > "HOLLight.hollight.REAL_LT_LADD_IMP"
994 "REAL_LT_LADD" > "HOLLight.hollight.REAL_LT_LADD"
995 "REAL_LT_INV_EQ" > "HOLLight.hollight.REAL_LT_INV_EQ"
996 "REAL_LT_INV2" > "HOLLight.hollight.REAL_LT_INV2"
997 "REAL_LT_INV" > "HOLLight.hollight.REAL_LT_INV"
998 "REAL_LT_IMP_NZ" > "HOLLight.hollight.REAL_LT_IMP_NZ"
999 "REAL_LT_IMP_NE" > "HOLLight.hollight.REAL_LT_IMP_NE"
1000 "REAL_LT_IMP_LE" > "HOLLight.hollight.REAL_LT_IMP_LE"
1001 "REAL_LT_GT" > "HOLLight.hollight.REAL_LT_GT"
1002 "REAL_LT_DIV2_EQ" > "HOLLight.hollight.REAL_LT_DIV2_EQ"
1003 "REAL_LT_DIV" > "HOLLight.hollight.REAL_LT_DIV"
1004 "REAL_LT_ANTISYM" > "HOLLight.hollight.REAL_LT_ANTISYM"
1005 "REAL_LT_ADD_SUB" > "HOLLight.hollight.REAL_LT_ADD_SUB"
1006 "REAL_LT_ADDR" > "HOLLight.hollight.REAL_LT_ADDR"
1007 "REAL_LT_ADDNEG2" > "HOLLight.hollight.REAL_LT_ADDNEG2"
1008 "REAL_LT_ADDNEG" > "HOLLight.hollight.REAL_LT_ADDNEG"
1009 "REAL_LT_ADDL" > "HOLLight.hollight.REAL_LT_ADDL"
1010 "REAL_LT_ADD2" > "HOLLight.hollight.REAL_LT_ADD2"
1011 "REAL_LT_ADD1" > "HOLLight.hollight.REAL_LT_ADD1"
1012 "REAL_LT_ADD" > "HOLLight.hollight.REAL_LT_ADD"
1013 "REAL_LT_01" > "HOLLight.hollight.REAL_LT_01"
1014 "REAL_LTE_TRANS" > "HOLLight.hollight.REAL_LTE_TRANS"
1015 "REAL_LTE_TOTAL" > "HOLLight.hollight.REAL_LTE_TOTAL"
1016 "REAL_LTE_ANTISYM" > "HOLLight.hollight.REAL_LTE_ANTISYM"
1017 "REAL_LTE_ADD2" > "HOLLight.hollight.REAL_LTE_ADD2"
1018 "REAL_LTE_ADD" > "HOLLight.hollight.REAL_LTE_ADD"
1019 "REAL_LNEG_UNIQ" > "HOLLight.hollight.REAL_LNEG_UNIQ"
1020 "REAL_LE_SUB_RADD" > "HOLLight.hollight.REAL_LE_SUB_RADD"
1021 "REAL_LE_SUB_LADD" > "HOLLight.hollight.REAL_LE_SUB_LADD"
1022 "REAL_LE_SQUARE_ABS" > "HOLLight.hollight.REAL_LE_SQUARE_ABS"
1023 "REAL_LE_SQUARE" > "HOLLight.hollight.REAL_LE_SQUARE"
1024 "REAL_LE_RNEG" > "HOLLight.hollight.REAL_LE_RNEG"
1025 "REAL_LE_RMUL_EQ" > "HOLLight.hollight.REAL_LE_RMUL_EQ"
1026 "REAL_LE_RMUL" > "HOLLight.hollight.REAL_LE_RMUL"
1027 "REAL_LE_RINV" > "HOLLight.hollight.REAL_LE_RINV"
1028 "REAL_LE_RDIV_EQ" > "HOLLight.hollight.REAL_LE_RDIV_EQ"
1029 "REAL_LE_RCANCEL_IMP" > "HOLLight.hollight.REAL_LE_RCANCEL_IMP"
1030 "REAL_LE_RADD" > "HOLLight.hollight.REAL_LE_RADD"
1031 "REAL_LE_POW_2" > "HOLLight.hollight.REAL_LE_POW_2"
1032 "REAL_LE_POW2" > "HOLLight.hollight.REAL_LE_POW2"
1033 "REAL_LE_NEGTOTAL" > "HOLLight.hollight.REAL_LE_NEGTOTAL"
1034 "REAL_LE_NEGR" > "HOLLight.hollight.REAL_LE_NEGR"
1035 "REAL_LE_NEGL" > "HOLLight.hollight.REAL_LE_NEGL"
1036 "REAL_LE_NEG2" > "HOLLight.hollight.REAL_LE_NEG2"
1037 "REAL_LE_NEG" > "HOLLight.hollight.REAL_LE_NEG"
1038 "REAL_LE_MUL_EQ" > "HOLLight.hollight.REAL_LE_MUL_EQ"
1039 "REAL_LE_MUL2" > "HOLLight.hollight.REAL_LE_MUL2"
1040 "REAL_LE_MIN" > "HOLLight.hollight.REAL_LE_MIN"
1041 "REAL_LE_MAX" > "HOLLight.hollight.REAL_LE_MAX"
1042 "REAL_LE_LT" > "HOLLight.hollight.REAL_LE_LT"
1043 "REAL_LE_LNEG" > "HOLLight.hollight.REAL_LE_LNEG"
1044 "REAL_LE_LMUL_EQ" > "HOLLight.hollight.REAL_LE_LMUL_EQ"
1045 "REAL_LE_LMUL" > "HOLLight.hollight.REAL_LE_LMUL"
1046 "REAL_LE_LINV" > "HOLLight.hollight.REAL_LE_LINV"
1047 "REAL_LE_LDIV_EQ" > "HOLLight.hollight.REAL_LE_LDIV_EQ"
1048 "REAL_LE_LCANCEL_IMP" > "HOLLight.hollight.REAL_LE_LCANCEL_IMP"
1049 "REAL_LE_LADD" > "HOLLight.hollight.REAL_LE_LADD"
1050 "REAL_LE_INV_EQ" > "HOLLight.hollight.REAL_LE_INV_EQ"
1051 "REAL_LE_INV2" > "HOLLight.hollight.REAL_LE_INV2"
1052 "REAL_LE_INV" > "HOLLight.hollight.REAL_LE_INV"
1053 "REAL_LE_DOUBLE" > "HOLLight.hollight.REAL_LE_DOUBLE"
1054 "REAL_LE_DIV2_EQ" > "HOLLight.hollight.REAL_LE_DIV2_EQ"
1055 "REAL_LE_DIV" > "HOLLight.hollight.REAL_LE_DIV"
1056 "REAL_LE_ADDR" > "HOLLight.hollight.REAL_LE_ADDR"
1057 "REAL_LE_ADDL" > "HOLLight.hollight.REAL_LE_ADDL"
1058 "REAL_LE_ADD2" > "HOLLight.hollight.REAL_LE_ADD2"
1059 "REAL_LE_ADD" > "HOLLight.hollight.REAL_LE_ADD"
1060 "REAL_LE_01" > "HOLLight.hollight.REAL_LE_01"
1061 "REAL_LET_TRANS" > "HOLLight.hollight.REAL_LET_TRANS"
1062 "REAL_LET_TOTAL" > "HOLLight.hollight.REAL_LET_TOTAL"
1063 "REAL_LET_ANTISYM" > "HOLLight.hollight.REAL_LET_ANTISYM"
1064 "REAL_LET_ADD2" > "HOLLight.hollight.REAL_LET_ADD2"
1065 "REAL_LET_ADD" > "HOLLight.hollight.REAL_LET_ADD"
1066 "REAL_INV_POW" > "HOLLight.hollight.REAL_INV_POW"
1067 "REAL_INV_NEG" > "HOLLight.hollight.REAL_INV_NEG"
1068 "REAL_INV_MUL" > "HOLLight.hollight.REAL_INV_MUL"
1069 "REAL_INV_LT_1" > "HOLLight.hollight.REAL_INV_LT_1"
1070 "REAL_INV_LE_1" > "HOLLight.hollight.REAL_INV_LE_1"
1071 "REAL_INV_INV" > "HOLLight.hollight.REAL_INV_INV"
1072 "REAL_INV_EQ_1" > "HOLLight.hollight.REAL_INV_EQ_1"
1073 "REAL_INV_EQ_0" > "HOLLight.hollight.REAL_INV_EQ_0"
1074 "REAL_INV_DIV" > "HOLLight.hollight.REAL_INV_DIV"
1075 "REAL_INV_1_LT" > "HOLLight.hollight.REAL_INV_1_LT"
1076 "REAL_INV_1_LE" > "HOLLight.hollight.REAL_INV_1_LE"
1077 "REAL_INV_1" > "HOLLight.hollight.REAL_INV_1"
1078 "REAL_INTEGRAL" > "HOLLight.hollight.REAL_INTEGRAL"
1079 "REAL_HREAL_LEMMA2" > "HOLLight.hollight.REAL_HREAL_LEMMA2"
1080 "REAL_HREAL_LEMMA1" > "HOLLight.hollight.REAL_HREAL_LEMMA1"
1081 "REAL_EQ_SUB_RADD" > "HOLLight.hollight.REAL_EQ_SUB_RADD"
1082 "REAL_EQ_SUB_LADD" > "HOLLight.hollight.REAL_EQ_SUB_LADD"
1083 "REAL_EQ_SQUARE_ABS" > "HOLLight.hollight.REAL_EQ_SQUARE_ABS"
1084 "REAL_EQ_RDIV_EQ" > "HOLLight.hollight.REAL_EQ_RDIV_EQ"
1085 "REAL_EQ_RCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_RCANCEL_IMP"
1086 "REAL_EQ_NEG2" > "HOLLight.hollight.REAL_EQ_NEG2"
1087 "REAL_EQ_MUL_RCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_RCANCEL"
1088 "REAL_EQ_MUL_LCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_LCANCEL"
1089 "REAL_EQ_LDIV_EQ" > "HOLLight.hollight.REAL_EQ_LDIV_EQ"
1090 "REAL_EQ_LCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_LCANCEL_IMP"
1091 "REAL_EQ_INV2" > "HOLLight.hollight.REAL_EQ_INV2"
1092 "REAL_EQ_IMP_LE" > "HOLLight.hollight.REAL_EQ_IMP_LE"
1093 "REAL_EQ_ADD_RCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL_0"
1094 "REAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL"
1095 "REAL_EQ_ADD_LCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL_0"
1096 "REAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL"
1097 "REAL_ENTIRE" > "HOLLight.hollight.REAL_ENTIRE"
1098 "REAL_DOWN2" > "HOLLight.hollight.REAL_DOWN2"
1099 "REAL_DOWN" > "HOLLight.hollight.REAL_DOWN"
1100 "REAL_DIV_RMUL" > "HOLLight.hollight.REAL_DIV_RMUL"
1101 "REAL_DIV_REFL" > "HOLLight.hollight.REAL_DIV_REFL"
1102 "REAL_DIV_POW2_ALT" > "HOLLight.hollight.REAL_DIV_POW2_ALT"
1103 "REAL_DIV_POW2" > "HOLLight.hollight.REAL_DIV_POW2"
1104 "REAL_DIV_LMUL" > "HOLLight.hollight.REAL_DIV_LMUL"
1105 "REAL_DIV_1" > "HOLLight.hollight.REAL_DIV_1"
1106 "REAL_DIFFSQ" > "HOLLight.hollight.REAL_DIFFSQ"
1107 "REAL_COMPLETE_SOMEPOS" > "HOLLight.hollight.REAL_COMPLETE_SOMEPOS"
1108 "REAL_COMPLETE" > "HOLLight.hollight.REAL_COMPLETE"
1109 "REAL_BOUNDS_LT" > "HOLLight.hollight.REAL_BOUNDS_LT"
1110 "REAL_BOUNDS_LE" > "HOLLight.hollight.REAL_BOUNDS_LE"
1111 "REAL_ADD_SUB2" > "HOLLight.hollight.REAL_ADD_SUB2"
1112 "REAL_ADD_SUB" > "HOLLight.hollight.REAL_ADD_SUB"
1113 "REAL_ADD_RINV" > "HOLLight.hollight.REAL_ADD_RINV"
1114 "REAL_ADD_RID" > "HOLLight.hollight.REAL_ADD_RID"
1115 "REAL_ADD_RDISTRIB" > "HOLLight.hollight.REAL_ADD_RDISTRIB"
1116 "REAL_ADD_AC" > "HOLLight.hollight.REAL_ADD_AC"
1117 "REAL_ADD2_SUB2" > "HOLLight.hollight.REAL_ADD2_SUB2"
1118 "REAL_ABS_ZERO" > "HOLLight.hollight.REAL_ABS_ZERO"
1119 "REAL_ABS_TRIANGLE_LT" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LT"
1120 "REAL_ABS_TRIANGLE_LE" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LE"
1121 "REAL_ABS_TRIANGLE" > "HOLLight.hollight.REAL_ABS_TRIANGLE"
1122 "REAL_ABS_SUB_ABS" > "HOLLight.hollight.REAL_ABS_SUB_ABS"
1123 "REAL_ABS_SUB" > "HOLLight.hollight.REAL_ABS_SUB"
1124 "REAL_ABS_STILLNZ" > "HOLLight.hollight.REAL_ABS_STILLNZ"
1125 "REAL_ABS_SIGN2" > "HOLLight.hollight.REAL_ABS_SIGN2"
1126 "REAL_ABS_SIGN" > "HOLLight.hollight.REAL_ABS_SIGN"
1127 "REAL_ABS_SGN" > "HOLLight.hollight.REAL_ABS_SGN"
1128 "REAL_ABS_REFL" > "HOLLight.hollight.REAL_ABS_REFL"
1129 "REAL_ABS_POW" > "HOLLight.hollight.REAL_ABS_POW"
1130 "REAL_ABS_POS" > "HOLLight.hollight.REAL_ABS_POS"
1131 "REAL_ABS_NZ" > "HOLLight.hollight.REAL_ABS_NZ"
1132 "REAL_ABS_NUM" > "HOLLight.hollight.REAL_ABS_NUM"
1133 "REAL_ABS_NEG" > "HOLLight.hollight.REAL_ABS_NEG"
1134 "REAL_ABS_MUL" > "HOLLight.hollight.REAL_ABS_MUL"
1135 "REAL_ABS_LE" > "HOLLight.hollight.REAL_ABS_LE"
1136 "REAL_ABS_INV" > "HOLLight.hollight.REAL_ABS_INV"
1137 "REAL_ABS_DIV" > "HOLLight.hollight.REAL_ABS_DIV"
1138 "REAL_ABS_CIRCLE" > "HOLLight.hollight.REAL_ABS_CIRCLE"
1139 "REAL_ABS_CASES" > "HOLLight.hollight.REAL_ABS_CASES"
1140 "REAL_ABS_BOUNDS" > "HOLLight.hollight.REAL_ABS_BOUNDS"
1141 "REAL_ABS_BOUND" > "HOLLight.hollight.REAL_ABS_BOUND"
1142 "REAL_ABS_BETWEEN2" > "HOLLight.hollight.REAL_ABS_BETWEEN2"
1143 "REAL_ABS_BETWEEN1" > "HOLLight.hollight.REAL_ABS_BETWEEN1"
1144 "REAL_ABS_BETWEEN" > "HOLLight.hollight.REAL_ABS_BETWEEN"
1145 "REAL_ABS_ABS" > "HOLLight.hollight.REAL_ABS_ABS"
1146 "REAL_ABS_1" > "HOLLight.hollight.REAL_ABS_1"
1147 "REAL_ABS_0" > "HOLLight.hollight.REAL_ABS_0"
1148 "RAT_LEMMA5" > "HOLLight.hollight.RAT_LEMMA5"
1149 "RAT_LEMMA4" > "HOLLight.hollight.RAT_LEMMA4"
1150 "RAT_LEMMA3" > "HOLLight.hollight.RAT_LEMMA3"
1151 "RAT_LEMMA2" > "HOLLight.hollight.RAT_LEMMA2"
1152 "RAT_LEMMA1" > "HOLLight.hollight.RAT_LEMMA1"
1153 "PSUBSET_UNIV" > "HOLLight.hollight.PSUBSET_UNIV"
1154 "PSUBSET_TRANS" > "Orderings.order_less_trans"
1155 "PSUBSET_SUBSET_TRANS" > "Orderings.order_less_le_trans"
1156 "PSUBSET_MEMBER" > "HOLLight.hollight.PSUBSET_MEMBER"
1157 "PSUBSET_IRREFL" > "Orderings.order_less_irrefl"
1158 "PSUBSET_INSERT_SUBSET" > "HOLLight.hollight.PSUBSET_INSERT_SUBSET"
1159 "PSUBSET_ALT" > "HOLLight.hollight.PSUBSET_ALT"
1160 "PRE_ELIM_THM" > "HOLLight.hollight.PRE_ELIM_THM"
1161 "POWERSET_CLAUSES" > "HOLLight.hollight.POWERSET_CLAUSES"
1162 "PASSOC_def" > "HOLLight.hollight.PASSOC_def"
1163 "PAIR_SURJECTIVE" > "Product_Type.prod.nchotomy"
1164 "PAIR_EXISTS_THM" > "HOLLight.hollight.PAIR_EXISTS_THM"
1165 "PAIR_EQ" > "Product_Type.Pair_eq"
1166 "PAIRWISE_def" > "HOLLight.hollight.PAIRWISE_def"
1167 "PAIRWISE_SING" > "HOLLight.hollight.PAIRWISE_SING"
1168 "PAIRWISE_MONO" > "HOLLight.hollight.PAIRWISE_MONO"
1169 "PAIRWISE_EMPTY" > "HOLLight.hollight.PAIRWISE_EMPTY"
1170 "PAIR" > "HOLLightCompat.PAIR"
1171 "OR_EXISTS_THM" > "HOL.ex_disj_distrib"
1172 "OR_CLAUSES" > "HOLLight.hollight.OR_CLAUSES"
1173 "ONE" > "Nat.One_nat_def"
1174 "ODD_SUB" > "HOLLight.hollight.ODD_SUB"
1175 "ODD_MULT" > "HOLLight.hollight.ODD_MULT"
1176 "ODD_MOD" > "HOLLight.hollight.ODD_MOD"
1177 "ODD_EXP" > "HOLLight.hollight.ODD_EXP"
1178 "ODD_EXISTS" > "Parity.odd_Suc_mult_two_ex"
1179 "ODD_DOUBLE" > "HOLLight.hollight.ODD_DOUBLE"
1180 "ODD_ADD" > "Parity.odd_add"
1181 "NUM_REP_def" > "HOLLight.hollight.NUM_REP_def"
1182 "NUM_OF_INT_OF_NUM" > "HOLLight.hollight.NUM_OF_INT_OF_NUM"
1183 "NUM_OF_INT" > "HOLLight.hollight.NUM_OF_INT"
1184 "NUM_INTEGRAL_LEMMA" > "HOLLight.hollight.NUM_INTEGRAL_LEMMA"
1185 "NUM_INTEGRAL" > "HOLLight.hollight.NUM_INTEGRAL"
1186 "NUM_GCD" > "HOLLight.hollight.NUM_GCD"
1187 "NUMSUM_def" > "HOLLight.hollight.NUMSUM_def"
1188 "NUMSUM_INJ" > "HOLLight.hollight.NUMSUM_INJ"
1189 "NUMSND_def" > "HOLLight.hollight.NUMSND_def"
1190 "NUMSEG_SING" > "SetInterval.order_class.atLeastAtMost_singleton"
1191 "NUMSEG_RREC" > "HOLLight.hollight.NUMSEG_RREC"
1192 "NUMSEG_REC" > "SetInterval.atLeastAtMostSuc_conv"
1193 "NUMSEG_OFFSET_IMAGE" > "SetInterval.image_add_atLeastAtMost"
1194 "NUMSEG_LT" > "HOLLight.hollight.NUMSEG_LT"
1195 "NUMSEG_LREC" > "HOLLight.hollight.NUMSEG_LREC"
1196 "NUMSEG_LE" > "HOLLight.hollight.NUMSEG_LE"
1197 "NUMSEG_EMPTY" > "HOLLight.hollight.NUMSEG_EMPTY"
1198 "NUMSEG_COMBINE_R" > "HOLLight.hollight.NUMSEG_COMBINE_R"
1199 "NUMSEG_COMBINE_L" > "HOLLight.hollight.NUMSEG_COMBINE_L"
1200 "NUMSEG_CLAUSES" > "HOLLight.hollight.NUMSEG_CLAUSES"
1201 "NUMSEG_ADD_SPLIT" > "HOLLight.hollight.NUMSEG_ADD_SPLIT"
1202 "NUMRIGHT_def" > "HOLLight.hollight.NUMRIGHT_def"
1203 "NUMPAIR_def" > "HOLLight.hollight.NUMPAIR_def"
1204 "NUMPAIR_INJ_LEMMA" > "HOLLight.hollight.NUMPAIR_INJ_LEMMA"
1205 "NUMPAIR_INJ" > "HOLLight.hollight.NUMPAIR_INJ"
1206 "NUMLEFT_def" > "HOLLight.hollight.NUMLEFT_def"
1207 "NUMFST_def" > "HOLLight.hollight.NUMFST_def"
1208 "NSUM_UNION_RZERO" > "HOLLight.hollight.NSUM_UNION_RZERO"
1209 "NSUM_UNION_NONZERO" > "HOLLight.hollight.NSUM_UNION_NONZERO"
1210 "NSUM_UNION_LZERO" > "HOLLight.hollight.NSUM_UNION_LZERO"
1211 "NSUM_UNION_EQ" > "HOLLight.hollight.NSUM_UNION_EQ"
1212 "NSUM_UNIONS_NONZERO" > "HOLLight.hollight.NSUM_UNIONS_NONZERO"
1213 "NSUM_UNION" > "HOLLight.hollight.NSUM_UNION"
1214 "NSUM_TRIV_NUMSEG" > "HOLLight.hollight.NSUM_TRIV_NUMSEG"
1215 "NSUM_SWAP_NUMSEG" > "HOLLight.hollight.NSUM_SWAP_NUMSEG"
1216 "NSUM_SWAP" > "HOLLight.hollight.NSUM_SWAP"
1217 "NSUM_SUPPORT" > "HOLLight.hollight.NSUM_SUPPORT"
1218 "NSUM_SUPERSET" > "HOLLight.hollight.NSUM_SUPERSET"
1219 "NSUM_SUBSET_SIMPLE" > "HOLLight.hollight.NSUM_SUBSET_SIMPLE"
1220 "NSUM_SUBSET" > "HOLLight.hollight.NSUM_SUBSET"
1221 "NSUM_SING_NUMSEG" > "HOLLight.hollight.NSUM_SING_NUMSEG"
1222 "NSUM_SING" > "HOLLight.hollight.NSUM_SING"
1223 "NSUM_RMUL" > "HOLLight.hollight.NSUM_RMUL"
1224 "NSUM_RESTRICT_SET" > "HOLLight.hollight.NSUM_RESTRICT_SET"
1225 "NSUM_RESTRICT" > "HOLLight.hollight.NSUM_RESTRICT"
1226 "NSUM_POS_BOUND" > "HOLLight.hollight.NSUM_POS_BOUND"
1227 "NSUM_PAIR" > "HOLLight.hollight.NSUM_PAIR"
1228 "NSUM_OFFSET_0" > "HOLLight.hollight.NSUM_OFFSET_0"
1229 "NSUM_OFFSET" > "HOLLight.hollight.NSUM_OFFSET"
1230 "NSUM_NSUM_RESTRICT" > "HOLLight.hollight.NSUM_NSUM_RESTRICT"
1231 "NSUM_NSUM_PRODUCT" > "HOLLight.hollight.NSUM_NSUM_PRODUCT"
1232 "NSUM_MULTICOUNT_GEN" > "HOLLight.hollight.NSUM_MULTICOUNT_GEN"
1233 "NSUM_MULTICOUNT" > "HOLLight.hollight.NSUM_MULTICOUNT"
1234 "NSUM_LT_ALL" > "HOLLight.hollight.NSUM_LT_ALL"
1235 "NSUM_LT" > "HOLLight.hollight.NSUM_LT"
1236 "NSUM_LMUL" > "HOLLight.hollight.NSUM_LMUL"
1237 "NSUM_LE_NUMSEG" > "HOLLight.hollight.NSUM_LE_NUMSEG"
1238 "NSUM_LE" > "HOLLight.hollight.NSUM_LE"
1239 "NSUM_INJECTION" > "HOLLight.hollight.NSUM_INJECTION"
1240 "NSUM_INCL_EXCL" > "HOLLight.hollight.NSUM_INCL_EXCL"
1241 "NSUM_IMAGE_NONZERO" > "HOLLight.hollight.NSUM_IMAGE_NONZERO"
1242 "NSUM_IMAGE_GEN" > "HOLLight.hollight.NSUM_IMAGE_GEN"
1243 "NSUM_IMAGE" > "HOLLight.hollight.NSUM_IMAGE"
1244 "NSUM_GROUP" > "HOLLight.hollight.NSUM_GROUP"
1245 "NSUM_EQ_SUPERSET" > "HOLLight.hollight.NSUM_EQ_SUPERSET"
1246 "NSUM_EQ_NUMSEG" > "HOLLight.hollight.NSUM_EQ_NUMSEG"
1247 "NSUM_EQ_GENERAL_INVERSES" > "HOLLight.hollight.NSUM_EQ_GENERAL_INVERSES"
1248 "NSUM_EQ_GENERAL" > "HOLLight.hollight.NSUM_EQ_GENERAL"
1249 "NSUM_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_NUMSEG"
1250 "NSUM_EQ_0_IFF_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_IFF_NUMSEG"
1251 "NSUM_EQ_0_IFF" > "HOLLight.hollight.NSUM_EQ_0_IFF"
1252 "NSUM_EQ_0" > "HOLLight.hollight.NSUM_EQ_0"
1253 "NSUM_EQ" > "HOLLight.hollight.NSUM_EQ"
1254 "NSUM_DIFF" > "HOLLight.hollight.NSUM_DIFF"
1255 "NSUM_DELTA" > "HOLLight.hollight.NSUM_DELTA"
1256 "NSUM_DELETE" > "HOLLight.hollight.NSUM_DELETE"
1257 "NSUM_CONST_NUMSEG" > "HOLLight.hollight.NSUM_CONST_NUMSEG"
1258 "NSUM_CONST" > "HOLLight.hollight.NSUM_CONST"
1259 "NSUM_CLOSED" > "HOLLight.hollight.NSUM_CLOSED"
1260 "NSUM_CLAUSES_RIGHT" > "HOLLight.hollight.NSUM_CLAUSES_RIGHT"
1261 "NSUM_CLAUSES_NUMSEG" > "HOLLight.hollight.NSUM_CLAUSES_NUMSEG"
1262 "NSUM_CLAUSES_LEFT" > "HOLLight.hollight.NSUM_CLAUSES_LEFT"
1263 "NSUM_CLAUSES" > "HOLLight.hollight.NSUM_CLAUSES"
1264 "NSUM_CASES" > "HOLLight.hollight.NSUM_CASES"
1265 "NSUM_BOUND_LT_GEN" > "HOLLight.hollight.NSUM_BOUND_LT_GEN"
1266 "NSUM_BOUND_LT_ALL" > "HOLLight.hollight.NSUM_BOUND_LT_ALL"
1267 "NSUM_BOUND_LT" > "HOLLight.hollight.NSUM_BOUND_LT"
1268 "NSUM_BOUND_GEN" > "HOLLight.hollight.NSUM_BOUND_GEN"
1269 "NSUM_BOUND" > "HOLLight.hollight.NSUM_BOUND"
1270 "NSUM_BIJECTION" > "HOLLight.hollight.NSUM_BIJECTION"
1271 "NSUM_ADD_SPLIT" > "HOLLight.hollight.NSUM_ADD_SPLIT"
1272 "NSUM_ADD_NUMSEG" > "HOLLight.hollight.NSUM_ADD_NUMSEG"
1273 "NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
1274 "NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
1275 "NSUM_0" > "HOLLight.hollight.NSUM_0"
1276 "NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
1277 "NOT_SUC" > "Nat.Suc_not_Zero"
1278 "NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
1279 "NOT_ODD" > "HOLLight.hollight.NOT_ODD"
1280 "NOT_LT" > "Orderings.linorder_class.not_less"
1281 "NOT_LE" > "Orderings.linorder_class.not_le"
1282 "NOT_IN_EMPTY" > "HOLLight.hollight.NOT_IN_EMPTY"
1283 "NOT_INSERT_EMPTY" > "Set.insert_not_empty"
1284 "NOT_FORALL_THM" > "HOL.not_all"
1285 "NOT_EXISTS_THM" > "HOL.not_ex"
1286 "NOT_EX" > "HOLLightList.NOT_EX"
1287 "NOT_EVEN" > "HOLLight.hollight.NOT_EVEN"
1288 "NOT_EQUAL_SETS" > "HOLLight.hollight.NOT_EQUAL_SETS"
1289 "NOT_EMPTY_INSERT" > "Set.empty_not_insert"
1290 "NOT_CONS_NIL" > "List.list.distinct_2"
1291 "NOT_CLAUSES_WEAK" > "HOLLight.hollight.NOT_CLAUSES_WEAK"
1292 "NOT_ALL" > "HOLLightList.NOT_ALL"
1293 "NEUTRAL_REAL_MUL" > "HOLLight.hollight.NEUTRAL_REAL_MUL"
1294 "NEUTRAL_REAL_ADD" > "HOLLight.hollight.NEUTRAL_REAL_ADD"
1295 "NEUTRAL_MUL" > "HOLLight.hollight.NEUTRAL_MUL"
1296 "NEUTRAL_ADD" > "HOLLight.hollight.NEUTRAL_ADD"
1297 "NADD_UBOUND" > "HOLLight.hollight.NADD_UBOUND"
1298 "NADD_SUC" > "HOLLight.hollight.NADD_SUC"
1299 "NADD_RDISTRIB" > "HOLLight.hollight.NADD_RDISTRIB"
1300 "NADD_OF_NUM_WELLDEF" > "HOLLight.hollight.NADD_OF_NUM_WELLDEF"
1301 "NADD_OF_NUM_MUL" > "HOLLight.hollight.NADD_OF_NUM_MUL"
1302 "NADD_OF_NUM_LE" > "HOLLight.hollight.NADD_OF_NUM_LE"
1303 "NADD_OF_NUM_EQ" > "HOLLight.hollight.NADD_OF_NUM_EQ"
1304 "NADD_OF_NUM_ADD" > "HOLLight.hollight.NADD_OF_NUM_ADD"
1305 "NADD_OF_NUM" > "HOLLight.hollight.NADD_OF_NUM"
1306 "NADD_NONZERO" > "HOLLight.hollight.NADD_NONZERO"
1307 "NADD_MUL_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_MUL_WELLDEF_LEMMA"
1308 "NADD_MUL_WELLDEF" > "HOLLight.hollight.NADD_MUL_WELLDEF"
1309 "NADD_MUL_SYM" > "HOLLight.hollight.NADD_MUL_SYM"
1310 "NADD_MUL_LINV_LEMMA8" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA8"
1311 "NADD_MUL_LINV_LEMMA7a" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7a"
1312 "NADD_MUL_LINV_LEMMA7" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7"
1313 "NADD_MUL_LINV_LEMMA6" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA6"
1314 "NADD_MUL_LINV_LEMMA5" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA5"
1315 "NADD_MUL_LINV_LEMMA4" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA4"
1316 "NADD_MUL_LINV_LEMMA3" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA3"
1317 "NADD_MUL_LINV_LEMMA2" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA2"
1318 "NADD_MUL_LINV_LEMMA1" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA1"
1319 "NADD_MUL_LINV_LEMMA0" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA0"
1320 "NADD_MUL_LINV" > "HOLLight.hollight.NADD_MUL_LINV"
1321 "NADD_MUL_LID" > "HOLLight.hollight.NADD_MUL_LID"
1322 "NADD_MUL_ASSOC" > "HOLLight.hollight.NADD_MUL_ASSOC"
1323 "NADD_MULTIPLICATIVE" > "HOLLight.hollight.NADD_MULTIPLICATIVE"
1324 "NADD_MUL" > "HOLLight.hollight.NADD_MUL"
1325 "NADD_LE_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_LE_WELLDEF_LEMMA"
1326 "NADD_LE_WELLDEF" > "HOLLight.hollight.NADD_LE_WELLDEF"
1327 "NADD_LE_TRANS" > "HOLLight.hollight.NADD_LE_TRANS"
1328 "NADD_LE_TOTAL_LEMMA" > "HOLLight.hollight.NADD_LE_TOTAL_LEMMA"
1329 "NADD_LE_TOTAL" > "HOLLight.hollight.NADD_LE_TOTAL"
1330 "NADD_LE_RMUL" > "HOLLight.hollight.NADD_LE_RMUL"
1331 "NADD_LE_REFL" > "HOLLight.hollight.NADD_LE_REFL"
1332 "NADD_LE_RADD" > "HOLLight.hollight.NADD_LE_RADD"
1333 "NADD_LE_LMUL" > "HOLLight.hollight.NADD_LE_LMUL"
1334 "NADD_LE_LADD" > "HOLLight.hollight.NADD_LE_LADD"
1335 "NADD_LE_EXISTS" > "HOLLight.hollight.NADD_LE_EXISTS"
1336 "NADD_LE_ANTISYM" > "HOLLight.hollight.NADD_LE_ANTISYM"
1337 "NADD_LE_ADD" > "HOLLight.hollight.NADD_LE_ADD"
1338 "NADD_LE_0" > "HOLLight.hollight.NADD_LE_0"
1339 "NADD_LDISTRIB" > "HOLLight.hollight.NADD_LDISTRIB"
1340 "NADD_LBOUND" > "HOLLight.hollight.NADD_LBOUND"
1341 "NADD_INV_WELLDEF" > "HOLLight.hollight.NADD_INV_WELLDEF"
1342 "NADD_INV_0" > "HOLLight.hollight.NADD_INV_0"
1343 "NADD_INV" > "HOLLight.hollight.NADD_INV"
1344 "NADD_EQ_TRANS" > "HOLLight.hollight.NADD_EQ_TRANS"
1345 "NADD_EQ_SYM" > "HOLLight.hollight.NADD_EQ_SYM"
1346 "NADD_EQ_REFL" > "HOLLight.hollight.NADD_EQ_REFL"
1347 "NADD_EQ_IMP_LE" > "HOLLight.hollight.NADD_EQ_IMP_LE"
1348 "NADD_DIST_LEMMA" > "HOLLight.hollight.NADD_DIST_LEMMA"
1349 "NADD_DIST" > "HOLLight.hollight.NADD_DIST"
1350 "NADD_COMPLETE" > "HOLLight.hollight.NADD_COMPLETE"
1351 "NADD_CAUCHY" > "HOLLight.hollight.NADD_CAUCHY"
1352 "NADD_BOUND" > "HOLLight.hollight.NADD_BOUND"
1353 "NADD_ARCH_ZERO" > "HOLLight.hollight.NADD_ARCH_ZERO"
1354 "NADD_ARCH_MULT" > "HOLLight.hollight.NADD_ARCH_MULT"
1355 "NADD_ARCH_LEMMA" > "HOLLight.hollight.NADD_ARCH_LEMMA"
1356 "NADD_ARCH" > "HOLLight.hollight.NADD_ARCH"
1357 "NADD_ALTMUL" > "HOLLight.hollight.NADD_ALTMUL"
1358 "NADD_ADD_WELLDEF" > "HOLLight.hollight.NADD_ADD_WELLDEF"
1359 "NADD_ADD_SYM" > "HOLLight.hollight.NADD_ADD_SYM"
1360 "NADD_ADD_LID" > "HOLLight.hollight.NADD_ADD_LID"
1361 "NADD_ADD_LCANCEL" > "HOLLight.hollight.NADD_ADD_LCANCEL"
1362 "NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
1363 "NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
1364 "NADD_ADD" > "HOLLight.hollight.NADD_ADD"
1365 "MULT_SYM" > "Fields.linordered_field_class.sign_simps_40"
1366 "MULT_SUC" > "Nat.mult_Suc_right"
1367 "MULT_EXP" > "Power.comm_monoid_mult_class.power_mult_distrib"
1368 "MULT_EQ_1" > "Nat.nat_mult_eq_1_iff"
1369 "MULT_EQ_0" > "Nat.mult_is_0"
1370 "MULT_DIV_LE" > "HOLLight.hollight.MULT_DIV_LE"
1371 "MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
1372 "MULT_ASSOC" > "Fields.linordered_field_class.sign_simps_41"
1373 "MULT_AC" > "HOLLight.hollight.MULT_AC"
1374 "MULT_2" > "Int.semiring_mult_2"
1375 "MULT_0" > "Divides.arithmetic_simps_41"
1376 "MONO_FORALL" > "Inductive.basic_monos_6"
1377 "MONO_EXISTS" > "Inductive.basic_monos_5"
1378 "MONO_COND" > "HOLLight.hollight.MONO_COND"
1379 "MONO_ALL2" > "List.list_all2_mono"
1380 "MONO_ALL" > "HOLLightList.MONO_ALL"
1381 "MONOIDAL_REAL_MUL" > "HOLLight.hollight.MONOIDAL_REAL_MUL"
1382 "MONOIDAL_REAL_ADD" > "HOLLight.hollight.MONOIDAL_REAL_ADD"
1383 "MONOIDAL_MUL" > "HOLLight.hollight.MONOIDAL_MUL"
1384 "MONOIDAL_ADD" > "HOLLight.hollight.MONOIDAL_ADD"
1385 "MONOIDAL_AC" > "HOLLight.hollight.MONOIDAL_AC"
1386 "MOD_UNIQ" > "HOLLight.hollight.MOD_UNIQ"
1387 "MOD_MULT_RMOD" > "HOLLight.hollight.MOD_MULT_RMOD"
1388 "MOD_MULT_MOD2" > "HOLLight.hollight.MOD_MULT_MOD2"
1389 "MOD_MULT_LMOD" > "HOLLight.hollight.MOD_MULT_LMOD"
1390 "MOD_MULT_ADD" > "Divides.mod_mult_self3"
1391 "MOD_MULT2" > "HOLLight.hollight.MOD_MULT2"
1392 "MOD_MOD_REFL" > "HOLLight.hollight.MOD_MOD_REFL"
1393 "MOD_MOD" > "HOLLight.hollight.MOD_MOD"
1394 "MOD_LT" > "Divides.mod_less"
1395 "MOD_LE" > "HOLLight.hollight.MOD_LE"
1396 "MOD_EXP_MOD" > "HOLLight.hollight.MOD_EXP_MOD"
1397 "MOD_EXISTS" > "HOLLight.hollight.MOD_EXISTS"
1398 "MOD_EQ_0" > "HOLLight.hollight.MOD_EQ_0"
1399 "MOD_EQ" > "HOLLight.hollight.MOD_EQ"
1400 "MOD_ADD_MOD" > "HOLLight.hollight.MOD_ADD_MOD"
1401 "MK_REC_INJ" > "HOLLight.hollight.MK_REC_INJ"
1402 "MINIMAL" > "HOLLight.hollight.MINIMAL"
1403 "MEM_MAP" > "HOLLightList.MEM_MAP"
1404 "MEM_FILTER" > "HOLLightList.MEM_FILTER"
1405 "MEM_EXISTS_EL" > "HOLLightList.MEM_EXISTS_EL"
1406 "MEM_EL" > "List.nth_mem"
1407 "MEM_APPEND" > "HOLLightList.MEM_APPEND"
1408 "MEMBER_NOT_EMPTY" > "Set.ex_in_conv"
1409 "MEASURE_LE" > "HOLLight.hollight.MEASURE_LE"
1410 "MATCH_SEQPATTERN" > "HOLLight.hollight.MATCH_SEQPATTERN"
1411 "MAP_o" > "List.map.compositionality"
1412 "MAP_SND_ZIP" > "List.map_snd_zip"
1413 "MAP_ID" > "List.map_ident"
1414 "MAP_I" > "List.map.id"
1415 "MAP_FST_ZIP" > "List.map_fst_zip"
1416 "MAP_EQ_NIL" > "List.map_is_Nil_conv"
1417 "MAP_EQ_DEGEN" > "HOLLightList.MAP_EQ_DEGEN"
1418 "MAP_EQ_ALL2" > "HOLLightList.MAP_EQ_ALL2"
1419 "MAP_EQ" > "HOLLightList.MAP_EQ"
1420 "MAP_APPEND" > "List.map_append"
1421 "MAP2" > "HOLLightList.MAP2"
1422 "LT_TRANS" > "Orderings.order_less_trans"
1423 "LT_SUC_LE" > "Nat.le_simps_2"
1424 "LT_SUC" > "Nat.Suc_less_eq"
1425 "LT_REFL" > "Nat.less_not_refl"
1426 "LT_NZ" > "Nat.neq0_conv"
1427 "LT_MULT_RCANCEL" > "HOLLight.hollight.LT_MULT_RCANCEL"
1428 "LT_MULT_LCANCEL" > "HOLLight.hollight.LT_MULT_LCANCEL"
1429 "LT_MULT2" > "HOLLight.hollight.LT_MULT2"
1430 "LT_MULT" > "Nat.nat_0_less_mult_iff"
1431 "LT_LMULT" > "HOLLight.hollight.LT_LMULT"
1432 "LT_LE" > "Nat.nat_less_le"
1433 "LT_IMP_LE" > "FunDef.termination_basic_simps_5"
1434 "LT_EXP" > "HOLLight.hollight.LT_EXP"
1435 "LT_EXISTS" > "HOLLight.hollight.LT_EXISTS"
1436 "LT_CASES" > "HOLLight.hollight.LT_CASES"
1437 "LT_ANTISYM" > "HOLLight.hollight.LT_ANTISYM"
1438 "LT_ADD_RCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_right"
1439 "LT_ADD_LCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_left"
1440 "LT_ADDR" > "HOLLight.hollight.LT_ADDR"
1441 "LT_ADD2" > "Groups.add_mono_thms_linordered_field_5"
1442 "LT_ADD" > "HOLLight.hollight.LT_ADD"
1443 "LT_0" > "Nat.zero_less_Suc"
1444 "LTE_TRANS" > "Orderings.order_less_le_trans"
1445 "LTE_CASES" > "HOLLight.hollight.LTE_CASES"
1446 "LTE_ANTISYM" > "HOLLight.hollight.LTE_ANTISYM"
1447 "LTE_ADD2" > "Groups.add_mono_thms_linordered_field_3"
1448 "LE_TRANS" > "Nat.le_trans"
1449 "LE_SUC_LT" > "Nat.Suc_le_eq"
1450 "LE_SUC" > "Nat.Suc_le_mono"
1451 "LE_SQUARE_REFL" > "Nat.le_square"
1452 "LE_REFL" > "Nat.le_refl"
1453 "LE_RDIV_EQ" > "HOLLight.hollight.LE_RDIV_EQ"
1454 "LE_MULT_RCANCEL" > "HOLLight.hollight.LE_MULT_RCANCEL"
1455 "LE_MULT_LCANCEL" > "HOLLight.hollight.LE_MULT_LCANCEL"
1456 "LE_MULT2" > "Nat.mult_le_mono"
1457 "LE_LT" > "Nat.le_eq_less_or_eq"
1458 "LE_LDIV_EQ" > "HOLLight.hollight.LE_LDIV_EQ"
1459 "LE_LDIV" > "HOLLight.hollight.LE_LDIV"
1460 "LE_EXP" > "HOLLight.hollight.LE_EXP"
1461 "LE_EXISTS" > "Nat.le_iff_add"
1462 "LE_CASES" > "Nat.nat_le_linear"
1463 "LE_C" > "HOLLight.hollight.LE_C"
1464 "LE_ANTISYM" > "Orderings.order_class.eq_iff"
1465 "LE_ADD_RCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_right"
1466 "LE_ADD_LCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left"
1467 "LE_ADDR" > "Nat.le_add2"
1468 "LE_ADD2" > "Groups.add_mono_thms_linordered_semiring_1"
1469 "LE_ADD" > "Nat.le_add1"
1470 "LE_1" > "HOLLight.hollight.LE_1"
1472 "LET_TRANS" > "Orderings.order_le_less_trans"
1473 "LET_END_def" > "HOLLight.hollight.LET_END_def"
1474 "LET_CASES" > "Orderings.linorder_class.le_less_linear"
1475 "LET_ANTISYM" > "HOLLight.hollight.LET_ANTISYM"
1476 "LET_ADD2" > "Groups.add_mono_thms_linordered_field_4"
1477 "LENGTH_TL" > "HOLLightList.LENGTH_TL"
1478 "LENGTH_REPLICATE" > "List.length_replicate"
1479 "LENGTH_MAP2" > "HOLLightList.LENGTH_MAP2"
1480 "LENGTH_MAP" > "List.length_map"
1481 "LENGTH_EQ_NIL" > "List.length_0_conv"
1482 "LENGTH_EQ_CONS" > "List.length_Suc_conv"
1483 "LENGTH_APPEND" > "List.length_append"
1484 "LEFT_SUB_DISTRIB" > "Nat.diff_mult_distrib2"
1485 "LEFT_OR_FORALL_THM" > "HOL.all_simps_3"
1486 "LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
1487 "LEFT_OR_DISTRIB" > "Groebner_Basis.dnf_1"
1488 "LEFT_IMP_FORALL_THM" > "HOL.ex_simps_5"
1489 "LEFT_IMP_EXISTS_THM" > "HOL.all_simps_5"
1490 "LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
1491 "LEFT_FORALL_IMP_THM" > "HOL.all_simps_5"
1492 "LEFT_EXISTS_IMP_THM" > "HOL.ex_simps_5"
1493 "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
1494 "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
1495 "LEFT_AND_EXISTS_THM" > "HOL.ex_simps_1"
1496 "LEFT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_25"
1497 "LAST_EL" > "List.last_conv_nth"
1498 "LAST_CLAUSES" > "HOLLightList.LAST_CLAUSES"
1499 "LAST_APPEND" > "List.last_append"
1500 "LAMBDA_UNIQUE" > "HOLLight.hollight.LAMBDA_UNIQUE"
1501 "LAMBDA_PAIR_THM" > "HOLLight.hollight.LAMBDA_PAIR_THM"
1502 "LAMBDA_ETA" > "HOLLight.hollight.LAMBDA_ETA"
1503 "LAMBDA_BETA" > "HOLLight.hollight.LAMBDA_BETA"
1504 "I_THM" > "HOL.refl"
1505 "I_O_ID" > "HOLLight.hollight.I_O_ID"
1506 "ITSET_def" > "HOLLight.hollight.ITSET_def"
1507 "ITSET_EQ" > "HOLLight.hollight.ITSET_EQ"
1508 "ITLIST_EXTRA" > "HOLLightList.ITLIST_EXTRA"
1509 "ITLIST_APPEND" > "List.foldr_append"
1510 "ITLIST2" > "HOLLightList.ITLIST2"
1511 "ITERATE_UNION_NONZERO" > "HOLLight.hollight.ITERATE_UNION_NONZERO"
1512 "ITERATE_UNION_GEN" > "HOLLight.hollight.ITERATE_UNION_GEN"
1513 "ITERATE_UNION" > "HOLLight.hollight.ITERATE_UNION"
1514 "ITERATE_SUPPORT" > "HOLLight.hollight.ITERATE_SUPPORT"
1515 "ITERATE_SUPERSET" > "HOLLight.hollight.ITERATE_SUPERSET"
1516 "ITERATE_SING" > "HOLLight.hollight.ITERATE_SING"
1517 "ITERATE_RELATED" > "HOLLight.hollight.ITERATE_RELATED"
1518 "ITERATE_PAIR" > "HOLLight.hollight.ITERATE_PAIR"
1519 "ITERATE_OP_GEN" > "HOLLight.hollight.ITERATE_OP_GEN"
1520 "ITERATE_OP" > "HOLLight.hollight.ITERATE_OP"
1521 "ITERATE_ITERATE_PRODUCT" > "HOLLight.hollight.ITERATE_ITERATE_PRODUCT"
1522 "ITERATE_INJECTION" > "HOLLight.hollight.ITERATE_INJECTION"
1523 "ITERATE_INCL_EXCL" > "HOLLight.hollight.ITERATE_INCL_EXCL"
1524 "ITERATE_IMAGE_NONZERO" > "HOLLight.hollight.ITERATE_IMAGE_NONZERO"
1525 "ITERATE_IMAGE" > "HOLLight.hollight.ITERATE_IMAGE"
1526 "ITERATE_EXPAND_CASES" > "HOLLight.hollight.ITERATE_EXPAND_CASES"
1527 "ITERATE_EQ_NEUTRAL" > "HOLLight.hollight.ITERATE_EQ_NEUTRAL"
1528 "ITERATE_EQ_GENERAL_INVERSES" > "HOLLight.hollight.ITERATE_EQ_GENERAL_INVERSES"
1529 "ITERATE_EQ_GENERAL" > "HOLLight.hollight.ITERATE_EQ_GENERAL"
1530 "ITERATE_EQ" > "HOLLight.hollight.ITERATE_EQ"
1531 "ITERATE_DIFF_GEN" > "HOLLight.hollight.ITERATE_DIFF_GEN"
1532 "ITERATE_DIFF" > "HOLLight.hollight.ITERATE_DIFF"
1533 "ITERATE_DELTA" > "HOLLight.hollight.ITERATE_DELTA"
1534 "ITERATE_DELETE" > "HOLLight.hollight.ITERATE_DELETE"
1535 "ITERATE_CLOSED" > "HOLLight.hollight.ITERATE_CLOSED"
1536 "ITERATE_CLAUSES_NUMSEG" > "HOLLight.hollight.ITERATE_CLAUSES_NUMSEG"
1537 "ITERATE_CLAUSES_GEN" > "HOLLight.hollight.ITERATE_CLAUSES_GEN"
1538 "ITERATE_CLAUSES" > "HOLLight.hollight.ITERATE_CLAUSES"
1539 "ITERATE_CASES" > "HOLLight.hollight.ITERATE_CASES"
1540 "ITERATE_BIJECTION" > "HOLLight.hollight.ITERATE_BIJECTION"
1541 "ISO_def" > "HOLLight.hollight.ISO_def"
1542 "ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
1543 "ISO_REFL" > "HOLLight.hollight.ISO_REFL"
1544 "ISO_FUN" > "HOLLight.hollight.ISO_FUN"
1545 "IN_UNIV" > "Set.UNIV_I"
1546 "IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
1547 "IN_UNION" > "Complete_Lattices.mem_simps_3"
1548 "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
1549 "IN_SING" > "Set.singleton_iff"
1550 "IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
1551 "IN_REST" > "HOLLight.hollight.IN_REST"
1552 "IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
1553 "IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
1554 "IN_INTERS" > "HOLLight.hollight.IN_INTERS"
1555 "IN_INTER" > "Complete_Lattices.mem_simps_4"
1556 "IN_INSERT" > "Complete_Lattices.mem_simps_1"
1557 "IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
1558 "IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
1559 "IN_ELIM_PAIR_THM" > "HOLLight.hollight.IN_ELIM_PAIR_THM"
1560 "IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
1561 "IN_DIFF" > "Complete_Lattices.mem_simps_6"
1562 "IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
1563 "IN_DELETE" > "HOLLight.hollight.IN_DELETE"
1564 "IN_CROSS" > "HOLLight.hollight.IN_CROSS"
1565 "INT_WOP" > "HOLLight.hollight.INT_WOP"
1566 "INT_POW" > "HOLLight.hollight.INT_POW"
1567 "INT_OF_NUM_OF_INT" > "HOLLight.hollight.INT_OF_NUM_OF_INT"
1568 "INT_LT_DISCRETE" > "HOLLight.hollight.INT_LT_DISCRETE"
1569 "INT_LT" > "HOLLight.hollight.INT_LT"
1570 "INT_INTEGRAL" > "HOLLight.hollight.INT_INTEGRAL"
1571 "INT_IMAGE" > "HOLLight.hollight.INT_IMAGE"
1572 "INT_GT_DISCRETE" > "HOLLight.hollight.INT_GT_DISCRETE"
1573 "INT_GT" > "HOLLight.hollight.INT_GT"
1574 "INT_GE" > "HOLLight.hollight.INT_GE"
1575 "INT_GCD_EXISTS_POS" > "HOLLight.hollight.INT_GCD_EXISTS_POS"
1576 "INT_GCD_EXISTS" > "HOLLight.hollight.INT_GCD_EXISTS"
1577 "INT_FORALL_POS" > "HOLLight.hollight.INT_FORALL_POS"
1578 "INT_FORALL_ABS" > "HOLLight.hollight.INT_FORALL_ABS"
1579 "INT_EXISTS_POS" > "HOLLight.hollight.INT_EXISTS_POS"
1580 "INT_EXISTS_ABS" > "HOLLight.hollight.INT_EXISTS_ABS"
1581 "INT_DIVMOD_UNIQ" > "HOLLight.hollight.INT_DIVMOD_UNIQ"
1582 "INT_DIVMOD_EXIST_0" > "HOLLight.hollight.INT_DIVMOD_EXIST_0"
1583 "INT_DIVISION" > "HOLLight.hollight.INT_DIVISION"
1584 "INT_ARCH" > "HOLLight.hollight.INT_ARCH"
1585 "INT_ABS_MUL_1" > "HOLLight.hollight.INT_ABS_MUL_1"
1586 "INT_ABS" > "HOLLight.hollight.INT_ABS"
1587 "INTER_UNIV" > "HOLLight.hollight.INTER_UNIV"
1588 "INTER_UNIONS" > "HOLLight.hollight.INTER_UNIONS"
1589 "INTER_SUBSET" > "HOLLight.hollight.INTER_SUBSET"
1590 "INTER_OVER_UNION" > "Lattices.distrib_lattice_class.distrib_1"
1591 "INTER_IDEMPOT" > "Big_Operators.lattice_class.Inf_fin.idem"
1592 "INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
1593 "INTER_COMM" > "Lattices.lattice_class.inf_sup_aci_1"
1594 "INTER_ASSOC" > "Lattices.lattice_class.inf_sup_aci_2"
1595 "INTER_ACI" > "HOLLight.hollight.INTER_ACI"
1596 "INTERS_UNIONS" > "HOLLight.hollight.INTERS_UNIONS"
1597 "INTERS_INSERT" > "Complete_Lattices.Inter_insert"
1598 "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
1599 "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
1600 "INTERS_2" > "Complete_Lattices.Int_eq_Inter"
1601 "INTERS_1" > "Complete_Lattices.complete_lattice_class.Inf_singleton"
1602 "INTERS_0" > "Complete_Lattices.Inter_empty"
1603 "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
1604 "INSERT_UNION_EQ" > "Set.Un_insert_left"
1605 "INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
1606 "INSERT_SUBSET" > "Set.insert_subset"
1607 "INSERT_INTER" > "Set.Int_insert_left"
1608 "INSERT_INSERT" > "Set.insert_absorb2"
1609 "INSERT_DIFF" > "Set.insert_Diff_if"
1610 "INSERT_DELETE" > "Set.insert_Diff"
1611 "INSERT_COMM" > "Set.insert_commute"
1612 "INSERT_AC" > "HOLLight.hollight.INSERT_AC"
1613 "INSERT" > "HOLLight.hollight.INSERT"
1614 "INJ_def" > "HOLLight.hollight.INJ_def"
1615 "INJ_INVERSE2" > "HOLLight.hollight.INJ_INVERSE2"
1616 "INJP_def" > "HOLLight.hollight.INJP_def"
1617 "INJP_INJ" > "HOLLight.hollight.INJP_INJ"
1618 "INJN_def" > "HOLLight.hollight.INJN_def"
1619 "INJN_INJ" > "HOLLight.hollight.INJN_INJ"
1620 "INJF_def" > "HOLLight.hollight.INJF_def"
1621 "INJF_INJ" > "HOLLight.hollight.INJF_INJ"
1622 "INJECTIVE_ON_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_ON_LEFT_INVERSE"
1623 "INJECTIVE_ON_IMAGE" > "HOLLight.hollight.INJECTIVE_ON_IMAGE"
1624 "INJECTIVE_MAP" > "HOLLightList.INJECTIVE_MAP"
1625 "INJECTIVE_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_LEFT_INVERSE"
1626 "INJECTIVE_IMAGE" > "HOLLight.hollight.INJECTIVE_IMAGE"
1627 "INJA_def" > "HOLLight.hollight.INJA_def"
1628 "INJA_INJ" > "HOLLight.hollight.INJA_INJ"
1629 "INFINITE_NONEMPTY" > "Infinite_Set.infinite_imp_nonempty"
1630 "INFINITE_IMAGE_INJ" > "HOLLight.hollight.INFINITE_IMAGE_INJ"
1631 "INFINITE_DIFF_FINITE" > "Infinite_Set.Diff_infinite_finite"
1632 "IND_SUC_def" > "HOLLight.hollight.IND_SUC_def"
1633 "IND_SUC_0_EXISTS" > "HOLLight.hollight.IND_SUC_0_EXISTS"
1634 "IND_0_def" > "HOLLight.hollight.IND_0_def"
1635 "IMP_EQ_CLAUSE" > "HOLLight.hollight.IMP_EQ_CLAUSE"
1636 "IMP_CONJ_ALT" > "HOLLight.hollight.IMP_CONJ_ALT"
1637 "IMP_CONJ" > "HOL.imp_conjL"
1638 "IMP_CLAUSES" > "HOLLight.hollight.IMP_CLAUSES"
1639 "IMAGE_o" > "Fun.image_compose"
1640 "IMAGE_UNIONS" > "HOLLight.hollight.IMAGE_UNIONS"
1641 "IMAGE_UNION" > "Set.image_Un"
1642 "IMAGE_SUBSET" > "Set.image_mono"
1643 "IMAGE_INTER_INJ" > "HOLLight.hollight.IMAGE_INTER_INJ"
1644 "IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
1645 "IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
1646 "IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
1647 "IMAGE_ID" > "Set.image_ident"
1648 "IMAGE_I" > "Fun.image_id"
1649 "IMAGE_EQ_EMPTY" > "Set.image_is_empty"
1650 "IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
1651 "IMAGE_DELETE_INJ" > "HOLLight.hollight.IMAGE_DELETE_INJ"
1652 "IMAGE_CONST" > "Set.image_constant_conv"
1653 "IMAGE_CLAUSES" > "HOLLight.hollight.IMAGE_CLAUSES"
1654 "HREAL_MUL_RZERO" > "HOLLight.hollight.HREAL_MUL_RZERO"
1655 "HREAL_MUL_LZERO" > "HOLLight.hollight.HREAL_MUL_LZERO"
1656 "HREAL_LE_MUL_RCANCEL_IMP" > "HOLLight.hollight.HREAL_LE_MUL_RCANCEL_IMP"
1657 "HREAL_LE_EXISTS_DEF" > "HOLLight.hollight.HREAL_LE_EXISTS_DEF"
1658 "HREAL_LE_ADD_RCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_RCANCEL"
1659 "HREAL_LE_ADD_LCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_LCANCEL"
1660 "HREAL_LE_ADD2" > "HOLLight.hollight.HREAL_LE_ADD2"
1661 "HREAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_RCANCEL"
1662 "HREAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_LCANCEL"
1663 "HREAL_ADD_RID" > "HOLLight.hollight.HREAL_ADD_RID"
1664 "HREAL_ADD_RDISTRIB" > "HOLLight.hollight.HREAL_ADD_RDISTRIB"
1665 "HREAL_ADD_AC" > "HOLLight.hollight.HREAL_ADD_AC"
1666 "HD_APPEND" > "List.hd_append"
1667 "HAS_SIZE_def" > "HOLLight.hollight.HAS_SIZE_def"
1668 "HAS_SIZE_UNIONS" > "HOLLight.hollight.HAS_SIZE_UNIONS"
1669 "HAS_SIZE_UNION" > "HOLLight.hollight.HAS_SIZE_UNION"
1670 "HAS_SIZE_SUC" > "HOLLight.hollight.HAS_SIZE_SUC"
1671 "HAS_SIZE_PRODUCT_DEPENDENT" > "HOLLight.hollight.HAS_SIZE_PRODUCT_DEPENDENT"
1672 "HAS_SIZE_PRODUCT" > "HOLLight.hollight.HAS_SIZE_PRODUCT"
1673 "HAS_SIZE_POWERSET" > "HOLLight.hollight.HAS_SIZE_POWERSET"
1674 "HAS_SIZE_NUMSEG_LT" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LT"
1675 "HAS_SIZE_NUMSEG_LE" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LE"
1676 "HAS_SIZE_NUMSEG_1" > "HOLLight.hollight.HAS_SIZE_NUMSEG_1"
1677 "HAS_SIZE_NUMSEG" > "HOLLight.hollight.HAS_SIZE_NUMSEG"
1678 "HAS_SIZE_INDEX" > "HOLLight.hollight.HAS_SIZE_INDEX"
1679 "HAS_SIZE_IMAGE_INJ_EQ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ_EQ"
1680 "HAS_SIZE_IMAGE_INJ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ"
1681 "HAS_SIZE_FUNSPACE" > "HOLLight.hollight.HAS_SIZE_FUNSPACE"
1682 "HAS_SIZE_FINITE_IMAGE" > "HOLLight.hollight.HAS_SIZE_FINITE_IMAGE"
1683 "HAS_SIZE_DIFF" > "HOLLight.hollight.HAS_SIZE_DIFF"
1684 "HAS_SIZE_CROSS" > "HOLLight.hollight.HAS_SIZE_CROSS"
1685 "HAS_SIZE_CLAUSES" > "HOLLight.hollight.HAS_SIZE_CLAUSES"
1686 "HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
1687 "HAS_SIZE_1" > "HOLLight.hollight.HAS_SIZE_1"
1688 "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
1689 "GE_C" > "HOLLight.hollight.GE_C"
1690 "FUN_IN_IMAGE" > "Set.imageI"
1691 "FUN_EQ_THM" > "HOL.fun_eq_iff"
1692 "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
1693 "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
1694 "FST" > "Product_Type.fst_conv"
1695 "FORALL_UNWIND_THM2" > "HOL.simp_thms_41"
1696 "FORALL_UNWIND_THM1" > "HOL.simp_thms_42"
1697 "FORALL_UNCURRY" > "HOLLight.hollight.FORALL_UNCURRY"
1698 "FORALL_TRIPLED_THM" > "HOLLight.hollight.FORALL_TRIPLED_THM"
1699 "FORALL_SUBSET_IMAGE" > "HOLLight.hollight.FORALL_SUBSET_IMAGE"
1700 "FORALL_SIMP" > "HOL.simp_thms_35"
1701 "FORALL_PAIR_THM" > "Product_Type.split_paired_All"
1702 "FORALL_PAIRED_THM" > "HOLLight.hollight.FORALL_PAIRED_THM"
1703 "FORALL_NOT_THM" > "HOL.not_ex"
1704 "FORALL_IN_UNIONS" > "HOLLight.hollight.FORALL_IN_UNIONS"
1705 "FORALL_IN_INSERT" > "HOLLight.hollight.FORALL_IN_INSERT"
1706 "FORALL_IN_IMAGE" > "HOLLight.hollight.FORALL_IN_IMAGE"
1707 "FORALL_IN_GSPEC" > "HOLLight.hollight.FORALL_IN_GSPEC"
1708 "FORALL_IN_CLAUSES" > "HOLLight.hollight.FORALL_IN_CLAUSES"
1709 "FORALL_FINITE_INDEX" > "HOLLight.hollight.FORALL_FINITE_INDEX"
1710 "FORALL_BOOL_THM" > "Set.all_bool_eq"
1711 "FORALL_AND_THM" > "HOL.all_conj_distrib"
1712 "FORALL_ALL" > "HOLLightList.FORALL_ALL"
1713 "FNIL_def" > "HOLLight.hollight.FNIL_def"
1714 "FINREC_def" > "HOLLight.hollight.FINREC_def"
1715 "FINREC_UNIQUE_LEMMA" > "HOLLight.hollight.FINREC_UNIQUE_LEMMA"
1716 "FINREC_SUC_LEMMA" > "HOLLight.hollight.FINREC_SUC_LEMMA"
1717 "FINREC_FUN_LEMMA" > "HOLLight.hollight.FINREC_FUN_LEMMA"
1718 "FINREC_FUN" > "HOLLight.hollight.FINREC_FUN"
1719 "FINREC_EXISTS_LEMMA" > "HOLLight.hollight.FINREC_EXISTS_LEMMA"
1720 "FINREC_1_LEMMA" > "HOLLight.hollight.FINREC_1_LEMMA"
1721 "FINITE_UNION_IMP" > "Finite_Set.finite_UnI"
1722 "FINITE_UNIONS" > "HOLLight.hollight.FINITE_UNIONS"
1723 "FINITE_UNION" > "Finite_Set.finite_Un"
1724 "FINITE_SUPPORT_DELTA" > "HOLLight.hollight.FINITE_SUPPORT_DELTA"
1725 "FINITE_SUPPORT" > "HOLLight.hollight.FINITE_SUPPORT"
1726 "FINITE_SUM_IMAGE" > "HOLLight.hollight.FINITE_SUM_IMAGE"
1727 "FINITE_SUBSET_IMAGE_IMP" > "HOLLight.hollight.FINITE_SUBSET_IMAGE_IMP"
1728 "FINITE_SUBSET_IMAGE" > "HOLLight.hollight.FINITE_SUBSET_IMAGE"
1729 "FINITE_SUBSET" > "Finite_Set.finite_subset"
1730 "FINITE_SING" > "HOLLight.hollight.FINITE_SING"
1731 "FINITE_RESTRICT" > "HOLLight.hollight.FINITE_RESTRICT"
1732 "FINITE_RECURSION_DELETE" > "HOLLight.hollight.FINITE_RECURSION_DELETE"
1733 "FINITE_RECURSION" > "HOLLight.hollight.FINITE_RECURSION"
1734 "FINITE_REAL_INTERVAL" > "HOLLight.hollight.FINITE_REAL_INTERVAL"
1735 "FINITE_PRODUCT_DEPENDENT" > "HOLLight.hollight.FINITE_PRODUCT_DEPENDENT"
1736 "FINITE_PRODUCT" > "HOLLight.hollight.FINITE_PRODUCT"
1737 "FINITE_POWERSET" > "HOLLight.hollight.FINITE_POWERSET"
1738 "FINITE_NUMSEG_LT" > "HOLLight.hollight.FINITE_NUMSEG_LT"
1739 "FINITE_NUMSEG_LE" > "HOLLight.hollight.FINITE_NUMSEG_LE"
1740 "FINITE_NUMSEG" > "SetInterval.finite_atLeastAtMost"
1741 "FINITE_INTSEG" > "HOLLight.hollight.FINITE_INTSEG"
1742 "FINITE_INTER" > "Finite_Set.finite_Int"
1743 "FINITE_INSERT" > "Finite_Set.finite_insert"
1744 "FINITE_INDUCT_STRONG" > "Finite_Set.finite_induct"
1745 "FINITE_INDUCT_DELETE" > "HOLLight.hollight.FINITE_INDUCT_DELETE"
1746 "FINITE_INDEX_WORKS" > "HOLLight.hollight.FINITE_INDEX_WORKS"
1747 "FINITE_INDEX_NUMSEG" > "HOLLight.hollight.FINITE_INDEX_NUMSEG"
1748 "FINITE_INDEX_NUMBERS" > "HOLLight.hollight.FINITE_INDEX_NUMBERS"
1749 "FINITE_INDEX_INRANGE" > "HOLLight.hollight.FINITE_INDEX_INRANGE"
1750 "FINITE_INDEX_INJ" > "HOLLight.hollight.FINITE_INDEX_INJ"
1751 "FINITE_IMAGE_INJ_GENERAL" > "HOLLight.hollight.FINITE_IMAGE_INJ_GENERAL"
1752 "FINITE_IMAGE_INJ_EQ" > "HOLLight.hollight.FINITE_IMAGE_INJ_EQ"
1753 "FINITE_IMAGE_INJ" > "HOLLight.hollight.FINITE_IMAGE_INJ"
1754 "FINITE_IMAGE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE_IMAGE"
1755 "FINITE_IMAGE_EXPAND" > "HOLLight.hollight.FINITE_IMAGE_EXPAND"
1756 "FINITE_IMAGE" > "Finite_Set.finite_imageI"
1757 "FINITE_HAS_SIZE" > "HOLLight.hollight.FINITE_HAS_SIZE"
1758 "FINITE_FUNSPACE" > "HOLLight.hollight.FINITE_FUNSPACE"
1759 "FINITE_FINITE_UNIONS" > "HOLLight.hollight.FINITE_FINITE_UNIONS"
1760 "FINITE_FINITE_PREIMAGE_GENERAL" > "HOLLight.hollight.FINITE_FINITE_PREIMAGE_GENERAL"
1761 "FINITE_FINITE_PREIMAGE" > "HOLLight.hollight.FINITE_FINITE_PREIMAGE"
1762 "FINITE_FINITE_IMAGE" > "HOLLight.hollight.FINITE_FINITE_IMAGE"
1763 "FINITE_EMPTY" > "Finite_Set.finite.emptyI"
1764 "FINITE_DIFF" > "Finite_Set.finite_Diff"
1765 "FINITE_DELETE_IMP" > "HOLLight.hollight.FINITE_DELETE_IMP"
1766 "FINITE_DELETE" > "HOLLight.hollight.FINITE_DELETE"
1767 "FINITE_CROSS" > "HOLLight.hollight.FINITE_CROSS"
1768 "FINITE_CART" > "HOLLight.hollight.FINITE_CART"
1769 "FILTER_MAP" > "List.filter_map"
1770 "FILTER_APPEND" > "List.filter_append"
1771 "FCONS_def" > "HOLLight.hollight.FCONS_def"
1772 "FCONS_UNDO" > "HOLLight.hollight.FCONS_UNDO"
1773 "FACT_NZ" > "Fact.fact_nonzero_nat"
1774 "FACT_MONO" > "Fact.fact_mono_nat"
1775 "FACT_LT" > "Fact.fact_gt_zero_nat"
1776 "FACT_LE" > "Fact.fact_ge_one_nat"
1777 "EX_MEM" > "HOLLightList.EX_MEM"
1778 "EX_IMP" > "HOLLightList.EX_IMP"
1779 "EXTENSION" > "Set.set_eq_iff"
1780 "EXP_ZERO" > "Power.power_0_left"
1781 "EXP_ONE" > "Power.monoid_mult_class.power_one"
1782 "EXP_MULT" > "Power.monoid_mult_class.power_mult"
1783 "EXP_MONO_LT_IMP" > "HOLLight.hollight.EXP_MONO_LT_IMP"
1784 "EXP_MONO_LT" > "HOLLight.hollight.EXP_MONO_LT"
1785 "EXP_MONO_LE_IMP" > "HOLLight.hollight.EXP_MONO_LE_IMP"
1786 "EXP_MONO_LE" > "HOLLight.hollight.EXP_MONO_LE"
1787 "EXP_MONO_EQ" > "HOLLight.hollight.EXP_MONO_EQ"
1788 "EXP_LT_0" > "HOLLight.hollight.EXP_LT_0"
1789 "EXP_EQ_1" > "HOLLight.hollight.EXP_EQ_1"
1790 "EXP_EQ_0" > "Power.power_eq_0_iff"
1791 "EXP_ADD" > "Power.monoid_mult_class.power_add"
1792 "EXP_2" > "Nat_Numeral.monoid_mult_class.power2_eq_square"
1793 "EXP_1" > "Power.monoid_mult_class.power_one_right"
1794 "EXISTS_UNIQUE_THM" > "HOLLightCompat.EXISTS_UNIQUE_THM"
1795 "EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
1796 "EXISTS_UNIQUE_ALT" > "HOLLight.hollight.EXISTS_UNIQUE_ALT"
1797 "EXISTS_UNIQUE" > "HOL.Ex1_def"
1798 "EXISTS_UNCURRY" > "HOLLight.hollight.EXISTS_UNCURRY"
1799 "EXISTS_TRIPLED_THM" > "HOLLight.hollight.EXISTS_TRIPLED_THM"
1800 "EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
1801 "EXISTS_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_SUBSET_IMAGE"
1802 "EXISTS_SIMP" > "HOL.simp_thms_36"
1803 "EXISTS_REFL" > "HOL.simp_thms_37"
1804 "EXISTS_PAIR_THM" > "Product_Type.split_paired_Ex"
1805 "EXISTS_PAIRED_THM" > "HOLLight.hollight.EXISTS_PAIRED_THM"
1806 "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
1807 "EXISTS_ONE_REP" > "HOLLight.hollight.EXISTS_ONE_REP"
1808 "EXISTS_NOT_THM" > "HOL.not_all"
1809 "EXISTS_IN_UNIONS" > "HOLLight.hollight.EXISTS_IN_UNIONS"
1810 "EXISTS_IN_INSERT" > "HOLLight.hollight.EXISTS_IN_INSERT"
1811 "EXISTS_IN_IMAGE" > "HOLLight.hollight.EXISTS_IN_IMAGE"
1812 "EXISTS_IN_GSPEC" > "HOLLight.hollight.EXISTS_IN_GSPEC"
1813 "EXISTS_IN_CLAUSES" > "HOLLight.hollight.EXISTS_IN_CLAUSES"
1814 "EXISTS_FINITE_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_FINITE_SUBSET_IMAGE"
1815 "EXISTS_EX" > "HOLLightList.EXISTS_EX"
1816 "EXISTS_BOOL_THM" > "Set.ex_bool_eq"
1817 "EXCLUDED_MIDDLE" > "HOLLight.hollight.EXCLUDED_MIDDLE"
1818 "EVEN_SUB" > "HOLLight.hollight.EVEN_SUB"
1819 "EVEN_OR_ODD" > "HOLLight.hollight.EVEN_OR_ODD"
1820 "EVEN_ODD_DECOMPOSITION" > "HOLLight.hollight.EVEN_ODD_DECOMPOSITION"
1821 "EVEN_MULT" > "Parity.even_product_nat"
1822 "EVEN_MOD" > "HOLLight.hollight.EVEN_MOD"
1823 "EVEN_EXP" > "HOLLight.hollight.EVEN_EXP"
1824 "EVEN_EXISTS_LEMMA" > "HOLLight.hollight.EVEN_EXISTS_LEMMA"
1825 "EVEN_EXISTS" > "Parity.even_mult_two_ex"
1826 "EVEN_DOUBLE" > "HOLLight.hollight.EVEN_DOUBLE"
1827 "EVEN_AND_ODD" > "HOLLight.hollight.EVEN_AND_ODD"
1828 "EVEN_ADD" > "Parity.even_add"
1829 "EQ_UNIV" > "HOLLight.hollight.EQ_UNIV"
1830 "EQ_TRANS" > "HOL.trans"
1831 "EQ_SYM_EQ" > "HOL.eq_ac_1"
1832 "EQ_SYM" > "HOL.eq_reflection"
1833 "EQ_REFL" > "HOL.refl"
1834 "EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
1835 "EQ_MULT_LCANCEL" > "Numeral_Simprocs.nat_mult_eq_cancel_disj"
1836 "EQ_IMP_LE" > "Nat.eq_imp_le"
1837 "EQ_EXT" > "HOL.eq_reflection"
1838 "EQ_EXP" > "HOLLight.hollight.EQ_EXP"
1839 "EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
1840 "EQ_ADD_RCANCEL_0" > "HOLLight.hollight.EQ_ADD_RCANCEL_0"
1841 "EQ_ADD_RCANCEL" > "Groups.cancel_semigroup_add_class.add_right_cancel"
1842 "EQ_ADD_LCANCEL_0" > "HOLLight.hollight.EQ_ADD_LCANCEL_0"
1843 "EQ_ADD_LCANCEL" > "Groups.cancel_semigroup_add_class.add_left_cancel"
1844 "EMPTY_UNIONS" > "HOLLight.hollight.EMPTY_UNIONS"
1845 "EMPTY_UNION" > "Lattices.bounded_lattice_bot_class.sup_eq_bot_iff"
1846 "EMPTY_SUBSET" > "Orderings.bot_class.bot_least"
1847 "EMPTY_NOT_UNIV" > "HOLLight.hollight.EMPTY_NOT_UNIV"
1848 "EMPTY_GSPEC" > "HOLLight.hollight.EMPTY_GSPEC"
1849 "EMPTY_DIFF" > "Set.empty_Diff"
1850 "EMPTY_DELETE" > "HOLLight.hollight.EMPTY_DELETE"
1851 "EL_CONS" > "List.nth_Cons'"
1852 "EL_APPEND" > "List.nth_append"
1853 "DIV_UNIQ" > "HOLLight.hollight.DIV_UNIQ"
1854 "DIV_REFL" > "Divides.semiring_div_class.div_self"
1855 "DIV_MUL_LE" > "HOLLight.hollight.DIV_MUL_LE"
1856 "DIV_MULT2" > "HOLLight.hollight.DIV_MULT2"
1857 "DIV_MONO_LT" > "HOLLight.hollight.DIV_MONO_LT"
1858 "DIV_MONO2" > "HOLLight.hollight.DIV_MONO2"
1859 "DIV_MONO" > "HOLLight.hollight.DIV_MONO"
1860 "DIV_MOD" > "HOLLight.hollight.DIV_MOD"
1861 "DIV_LT" > "Divides.div_less"
1862 "DIV_LE_EXCLUSION" > "HOLLight.hollight.DIV_LE_EXCLUSION"
1863 "DIV_LE" > "HOLLight.hollight.DIV_LE"
1864 "DIV_EQ_EXCLUSION" > "HOLLight.hollight.DIV_EQ_EXCLUSION"
1865 "DIV_EQ_0" > "HOLLight.hollight.DIV_EQ_0"
1866 "DIV_DIV" > "HOLLight.hollight.DIV_DIV"
1867 "DIV_ADD_MOD" > "HOLLight.hollight.DIV_ADD_MOD"
1868 "DIVMOD_UNIQ_LEMMA" > "HOLLight.hollight.DIVMOD_UNIQ_LEMMA"
1869 "DIVMOD_UNIQ" > "HOLLight.hollight.DIVMOD_UNIQ"
1870 "DIVMOD_EXIST_0" > "HOLLight.hollight.DIVMOD_EXIST_0"
1871 "DIVMOD_EXIST" > "HOLLight.hollight.DIVMOD_EXIST"
1872 "DIVMOD_ELIM_THM" > "HOLLight.hollight.DIVMOD_ELIM_THM"
1873 "DIVISION" > "HOLLight.hollight.DIVISION"
1874 "DIST_TRIANGLE_LE" > "HOLLight.hollight.DIST_TRIANGLE_LE"
1875 "DIST_TRIANGLES_LE" > "HOLLight.hollight.DIST_TRIANGLES_LE"
1876 "DIST_SYM" > "HOLLight.hollight.DIST_SYM"
1877 "DIST_RZERO" > "HOLLight.hollight.DIST_RZERO"
1878 "DIST_RMUL" > "HOLLight.hollight.DIST_RMUL"
1879 "DIST_REFL" > "HOLLight.hollight.DIST_REFL"
1880 "DIST_RADD_0" > "HOLLight.hollight.DIST_RADD_0"
1881 "DIST_RADD" > "HOLLight.hollight.DIST_RADD"
1882 "DIST_LZERO" > "HOLLight.hollight.DIST_LZERO"
1883 "DIST_LMUL" > "HOLLight.hollight.DIST_LMUL"
1884 "DIST_LE_CASES" > "HOLLight.hollight.DIST_LE_CASES"
1885 "DIST_LADD_0" > "HOLLight.hollight.DIST_LADD_0"
1886 "DIST_LADD" > "HOLLight.hollight.DIST_LADD"
1887 "DIST_EQ_0" > "HOLLight.hollight.DIST_EQ_0"
1888 "DIST_ELIM_THM" > "HOLLight.hollight.DIST_ELIM_THM"
1889 "DISJ_SYM" > "Groebner_Basis.dnf_4"
1890 "DISJ_ASSOC" > "HOL.disj_ac_3"
1891 "DISJ_ACI" > "HOLLight.hollight.DISJ_ACI"
1892 "DISJOINT_UNION" > "HOLLight.hollight.DISJOINT_UNION"
1893 "DISJOINT_SYM" > "HOLLight.hollight.DISJOINT_SYM"
1894 "DISJOINT_NUMSEG" > "HOLLight.hollight.DISJOINT_NUMSEG"
1895 "DISJOINT_INSERT" > "HOLLight.hollight.DISJOINT_INSERT"
1896 "DISJOINT_EMPTY_REFL" > "HOLLight.hollight.DISJOINT_EMPTY_REFL"
1897 "DISJOINT_EMPTY" > "HOLLight.hollight.DISJOINT_EMPTY"
1898 "DISJOINT_DELETE_SYM" > "HOLLight.hollight.DISJOINT_DELETE_SYM"
1899 "DIMINDEX_UNIV" > "HOLLight.hollight.DIMINDEX_UNIV"
1900 "DIMINDEX_UNIQUE" > "HOLLight.hollight.DIMINDEX_UNIQUE"
1901 "DIMINDEX_NONZERO" > "HOLLight.hollight.DIMINDEX_NONZERO"
1902 "DIMINDEX_GE_1" > "HOLLight.hollight.DIMINDEX_GE_1"
1903 "DIMINDEX_FINITE_IMAGE" > "HOLLight.hollight.DIMINDEX_FINITE_IMAGE"
1904 "DIFF_UNIV" > "Set.Diff_UNIV"
1905 "DIFF_INTERS" > "HOLLight.hollight.DIFF_INTERS"
1906 "DIFF_INSERT" > "Set.Diff_insert2"
1907 "DIFF_EQ_EMPTY" > "Set.Diff_cancel"
1908 "DIFF_EMPTY" > "Set.Diff_empty"
1909 "DIFF_DIFF" > "Set.Diff_idemp"
1910 "DEST_REC_INJ" > "HOLLight.hollight.recspace._dest_rec_inject"
1911 "DELETE_SUBSET" > "HOLLight.hollight.DELETE_SUBSET"
1912 "DELETE_NON_ELEMENT" > "HOLLight.hollight.DELETE_NON_ELEMENT"
1913 "DELETE_INTER" > "HOLLight.hollight.DELETE_INTER"
1914 "DELETE_INSERT" > "HOLLight.hollight.DELETE_INSERT"
1915 "DELETE_DELETE" > "HOLLight.hollight.DELETE_DELETE"
1916 "DELETE_COMM" > "HOLLight.hollight.DELETE_COMM"
1917 "DEF_~" > "Groebner_Basis.bool_simps_19"
1918 "DEF_vector" > "HOLLight.hollight.DEF_vector"
1919 "DEF_treal_of_num" > "HOLLight.hollight.DEF_treal_of_num"
1920 "DEF_treal_neg" > "HOLLight.hollight.DEF_treal_neg"
1921 "DEF_treal_mul" > "HOLLight.hollight.DEF_treal_mul"
1922 "DEF_treal_le" > "HOLLight.hollight.DEF_treal_le"
1923 "DEF_treal_inv" > "HOLLight.hollight.DEF_treal_inv"
1924 "DEF_treal_eq" > "HOLLight.hollight.DEF_treal_eq"
1925 "DEF_treal_add" > "HOLLight.hollight.DEF_treal_add"
1926 "DEF_tailadmissible" > "HOLLight.hollight.DEF_tailadmissible"
1927 "DEF_support" > "HOLLight.hollight.DEF_support"
1928 "DEF_superadmissible" > "HOLLight.hollight.DEF_superadmissible"
1929 "DEF_sum" > "HOLLight.hollight.DEF_sum"
1930 "DEF_sndcart" > "HOLLight.hollight.DEF_sndcart"
1931 "DEF_set_of_list" > "HOLLightList.DEF_set_of_list"
1932 "DEF_rem" > "HOLLight.hollight.DEF_rem"
1933 "DEF_real_sub" > "HOLLight.hollight.DEF_real_sub"
1934 "DEF_real_sgn" > "HOLLight.hollight.DEF_real_sgn"
1935 "DEF_real_pow" > "HOLLight.hollight.DEF_real_pow"
1936 "DEF_real_of_num" > "HOLLight.hollight.DEF_real_of_num"
1937 "DEF_real_neg" > "HOLLight.hollight.DEF_real_neg"
1938 "DEF_real_mul" > "HOLLight.hollight.DEF_real_mul"
1939 "DEF_real_mod" > "HOLLight.hollight.DEF_real_mod"
1940 "DEF_real_min" > "HOLLight.hollight.DEF_real_min"
1941 "DEF_real_max" > "HOLLight.hollight.DEF_real_max"
1942 "DEF_real_lt" > "HOLLight.hollight.DEF_real_lt"
1943 "DEF_real_le" > "HOLLight.hollight.DEF_real_le"
1944 "DEF_real_inv" > "HOLLight.hollight.DEF_real_inv"
1945 "DEF_real_gt" > "HOLLight.hollight.DEF_real_gt"
1946 "DEF_real_ge" > "HOLLight.hollight.DEF_real_ge"
1947 "DEF_real_div" > "HOLLight.hollight.DEF_real_div"
1948 "DEF_real_add" > "HOLLight.hollight.DEF_real_add"
1949 "DEF_real_abs" > "HOLLight.hollight.DEF_real_abs"
1950 "DEF_pastecart" > "HOLLight.hollight.DEF_pastecart"
1951 "DEF_pairwise" > "HOLLight.hollight.DEF_pairwise"
1952 "DEF_o" > "Fun.comp_def"
1953 "DEF_num_of_int" > "HOLLight.hollight.DEF_num_of_int"
1954 "DEF_num_mod" > "HOLLight.hollight.DEF_num_mod"
1955 "DEF_num_gcd" > "HOLLight.hollight.DEF_num_gcd"
1956 "DEF_num_divides" > "HOLLight.hollight.DEF_num_divides"
1957 "DEF_num_coprime" > "HOLLight.hollight.DEF_num_coprime"
1958 "DEF_nsum" > "HOLLight.hollight.DEF_nsum"
1959 "DEF_neutral" > "HOLLight.hollight.DEF_neutral"
1960 "DEF_nadd_rinv" > "HOLLight.hollight.DEF_nadd_rinv"
1961 "DEF_nadd_of_num" > "HOLLight.hollight.DEF_nadd_of_num"
1962 "DEF_nadd_mul" > "HOLLight.hollight.DEF_nadd_mul"
1963 "DEF_nadd_le" > "HOLLight.hollight.DEF_nadd_le"
1964 "DEF_nadd_inv" > "HOLLight.hollight.DEF_nadd_inv"
1965 "DEF_nadd_eq" > "HOLLight.hollight.DEF_nadd_eq"
1966 "DEF_nadd_add" > "HOLLight.hollight.DEF_nadd_add"
1967 "DEF_monoidal" > "HOLLight.hollight.DEF_monoidal"
1968 "DEF_minimal" > "HOLLight.hollight.DEF_minimal"
1969 "DEF_lambda" > "HOLLight.hollight.DEF_lambda"
1970 "DEF_iterate" > "HOLLight.hollight.DEF_iterate"
1971 "DEF_is_nadd" > "HOLLight.hollight.DEF_is_nadd"
1972 "DEF_integer" > "HOLLight.hollight.DEF_integer"
1973 "DEF_int_sub" > "HOLLight.hollight.DEF_int_sub"
1974 "DEF_int_sgn" > "HOLLight.hollight.DEF_int_sgn"
1975 "DEF_int_pow" > "HOLLight.hollight.DEF_int_pow"
1976 "DEF_int_of_num" > "HOLLight.hollight.DEF_int_of_num"
1977 "DEF_int_neg" > "HOLLight.hollight.DEF_int_neg"
1978 "DEF_int_mul" > "HOLLight.hollight.DEF_int_mul"
1979 "DEF_int_mod" > "HOLLight.hollight.DEF_int_mod"
1980 "DEF_int_min" > "HOLLight.hollight.DEF_int_min"
1981 "DEF_int_max" > "HOLLight.hollight.DEF_int_max"
1982 "DEF_int_lt" > "HOLLight.hollight.DEF_int_lt"
1983 "DEF_int_le" > "HOLLight.hollight.DEF_int_le"
1984 "DEF_int_gt" > "HOLLight.hollight.DEF_int_gt"
1985 "DEF_int_ge" > "HOLLight.hollight.DEF_int_ge"
1986 "DEF_int_gcd" > "HOLLight.hollight.DEF_int_gcd"
1987 "DEF_int_divides" > "HOLLight.hollight.DEF_int_divides"
1988 "DEF_int_coprime" > "HOLLight.hollight.DEF_int_coprime"
1989 "DEF_int_add" > "HOLLight.hollight.DEF_int_add"
1990 "DEF_int_abs" > "HOLLight.hollight.DEF_int_abs"
1991 "DEF_hreal_of_num" > "HOLLight.hollight.DEF_hreal_of_num"
1992 "DEF_hreal_mul" > "HOLLight.hollight.DEF_hreal_mul"
1993 "DEF_hreal_le" > "HOLLight.hollight.DEF_hreal_le"
1994 "DEF_hreal_inv" > "HOLLight.hollight.DEF_hreal_inv"
1995 "DEF_hreal_add" > "HOLLight.hollight.DEF_hreal_add"
1996 "DEF_fstcart" > "HOLLight.hollight.DEF_fstcart"
1997 "DEF_div" > "HOLLight.hollight.DEF_div"
1998 "DEF_dist" > "HOLLight.hollight.DEF_dist"
1999 "DEF_dimindex" > "HOLLight.hollight.DEF_dimindex"
2000 "DEF_admissible" > "HOLLight.hollight.DEF_admissible"
2001 "DEF__star_" > "HOLLightCompat.DEF__star_"
2002 "DEF__slash__backslash_" > "HOLLightCompat.DEF__slash__backslash_"
2003 "DEF__questionmark__exclamationmark_" > "HOLLightCompat.EXISTS_UNIQUE_THM"
2004 "DEF__questionmark_" > "HOL.Ex_def"
2005 "DEF__lessthan__equal__c" > "HOLLight.hollight.DEF__lessthan__equal__c"
2006 "DEF__lessthan__equal_" > "HOLLightCompat.DEF__lessthan__equal_"
2007 "DEF__lessthan__c" > "HOLLight.hollight.DEF__lessthan__c"
2008 "DEF__lessthan_" > "HOLLightCompat.DEF__lessthan_"
2009 "DEF__greaterthan__equal__c" > "HOLLight.hollight.DEF__greaterthan__equal__c"
2010 "DEF__greaterthan__equal_" > "HOLLightCompat.DEF__greaterthan__equal_"
2011 "DEF__greaterthan__c" > "HOLLight.hollight.DEF__greaterthan__c"
2012 "DEF__greaterthan_" > "HOLLightCompat.DEF__greaterthan_"
2013 "DEF__exclamationmark_" > "HOL.All_def"
2014 "DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
2015 "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
2016 "DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
2017 "DEF__dot__dot_" > "HOLLightCompat.dotdot_def"
2018 "DEF__backslash__slash_" > "HOL.or_def"
2019 "DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
2020 "DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
2021 "DEF__MATCH" > "HOLLight.hollight.DEF__MATCH"
2022 "DEF__GUARDED_PATTERN" > "HOLLight.hollight.DEF__GUARDED_PATTERN"
2023 "DEF__FUNCTION" > "HOLLight.hollight.DEF__FUNCTION"
2024 "DEF__FALSITY_" > "HOLLight.hollight.DEF__FALSITY_"
2025 "DEF__11937" > "HOLLight.hollight.DEF__11937"
2026 "DEF_ZRECSPACE" > "HOLLight.hollight.DEF_ZRECSPACE"
2027 "DEF_ZCONSTR" > "HOLLight.hollight.DEF_ZCONSTR"
2028 "DEF_ZBOT" > "HOLLight.hollight.DEF_ZBOT"
2029 "DEF_WF" > "HOLLightCompat.DEF_WF"
2030 "DEF_UNIV" > "HOLLightCompat.DEF_UNIV"
2031 "DEF_UNIONS" > "HOLLightCompat.DEF_UNIONS"
2032 "DEF_UNION" > "HOLLightCompat.DEF_UNION"
2033 "DEF_UNCURRY" > "HOLLight.hollight.DEF_UNCURRY"
2034 "DEF_T" > "HOL.True_def"
2035 "DEF_SURJ" > "HOLLight.hollight.DEF_SURJ"
2036 "DEF_SUBSET" > "HOLLightCompat.DEF_SUBSET"
2037 "DEF_SND" > "HOLLightCompat.DEF_SND"
2038 "DEF_SING" > "HOLLight.hollight.DEF_SING"
2039 "DEF_SETSPEC" > "HOLLightCompat.SETSPEC_def"
2040 "DEF_REVERSE" > "HOLLightList.DEF_REVERSE"
2041 "DEF_REST" > "HOLLight.hollight.DEF_REST"
2042 "DEF_REPLICATE" > "HOLLightList.DEF_REPLICATE"
2043 "DEF_PSUBSET" > "HOLLightCompat.DEF_PSUBSET"
2044 "DEF_PRE" > "HOLLightCompat.DEF_PRE"
2045 "DEF_PASSOC" > "HOLLight.hollight.DEF_PASSOC"
2046 "DEF_PAIRWISE" > "HOLLight.hollight.DEF_PAIRWISE"
2047 "DEF_ONTO" > "Fun.surj_def"
2048 "DEF_ONE_ONE" > "HOLLightCompat.DEF_ONE_ONE"
2049 "DEF_ODD" > "HOLLightCompat.DEF_ODD"
2050 "DEF_NUM_REP" > "HOLLight.hollight.DEF_NUM_REP"
2051 "DEF_NUMSUM" > "HOLLight.hollight.DEF_NUMSUM"
2052 "DEF_NUMSND" > "HOLLight.hollight.DEF_NUMSND"
2053 "DEF_NUMRIGHT" > "HOLLight.hollight.DEF_NUMRIGHT"
2054 "DEF_NUMPAIR" > "HOLLight.hollight.DEF_NUMPAIR"
2055 "DEF_NUMLEFT" > "HOLLight.hollight.DEF_NUMLEFT"
2056 "DEF_NUMFST" > "HOLLight.hollight.DEF_NUMFST"
2057 "DEF_NUMERAL" > "HOLLightCompat.NUMERAL_def"
2058 "DEF_NULL" > "HOLLightList.DEF_NULL"
2059 "DEF_MOD" > "HOLLightCompat.DEF_MOD"
2060 "DEF_MIN" > "Orderings.ord_class.min_def"
2061 "DEF_MEM" > "HOLLightList.DEF_MEM"
2062 "DEF_MEASURE" > "HOLLightCompat.MEASURE_def"
2063 "DEF_MAX" > "Orderings.ord_class.max_def"
2064 "DEF_MAP" > "HOLLightList.DEF_MAP"
2065 "DEF_LET_END" > "HOLLight.hollight.DEF_LET_END"
2066 "DEF_LET" > "HOLLightCompat.LET_def"
2067 "DEF_LENGTH" > "HOLLightList.DEF_LENGTH"
2068 "DEF_LAST" > "HOLLightList.DEF_LAST"
2069 "DEF_ITSET" > "HOLLight.hollight.DEF_ITSET"
2070 "DEF_ITLIST" > "HOLLightList.DEF_ITLIST"
2071 "DEF_ISO" > "HOLLight.hollight.DEF_ISO"
2072 "DEF_INTERS" > "HOLLightCompat.DEF_INTERS"
2073 "DEF_INTER" > "HOLLightCompat.DEF_INTER"
2074 "DEF_INSERT" > "HOLLightCompat.DEF_INSERT"
2075 "DEF_INJP" > "HOLLight.hollight.DEF_INJP"
2076 "DEF_INJN" > "HOLLight.hollight.DEF_INJN"
2077 "DEF_INJF" > "HOLLight.hollight.DEF_INJF"
2078 "DEF_INJA" > "HOLLight.hollight.DEF_INJA"
2079 "DEF_INJ" > "HOLLight.hollight.DEF_INJ"
2080 "DEF_INFINITE" > "HOLLightCompat.DEF_INFINITE"
2081 "DEF_IND_SUC" > "HOLLight.hollight.DEF_IND_SUC"
2082 "DEF_IND_0" > "HOLLight.hollight.DEF_IND_0"
2083 "DEF_IN" > "Set.mem_def"
2084 "DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
2085 "DEF_I" > "Fun.id_apply"
2086 "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
2087 "DEF_GSPEC" > "Set.Collect_def"
2088 "DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
2089 "DEF_GABS" > "HOLLightCompat.DEF_GABS"
2090 "DEF_FST" > "HOLLightCompat.DEF_FST"
2091 "DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
2092 "DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"
2093 "DEF_FINITE" > "HOLLightCompat.DEF_FINITE"
2094 "DEF_FILTER" > "HOLLightList.DEF_FILTER"
2095 "DEF_FCONS" > "HOLLight.hollight.DEF_FCONS"
2096 "DEF_FACT" > "HOLLightCompat.DEF_FACT"
2097 "DEF_F" > "HOL.False_def"
2098 "DEF_EXP" > "HOLLightCompat.DEF_EXP"
2099 "DEF_EX" > "HOLLightList.DEF_EX"
2100 "DEF_EVEN" > "HOLLightCompat.DEF_EVEN"
2101 "DEF_EMPTY" > "HOLLightCompat.DEF_EMPTY"
2102 "DEF_EL" > "HOLLightList.DEF_EL"
2103 "DEF_DIV" > "HOLLightCompat.DEF_DIV"
2104 "DEF_DISJOINT" > "HOLLightCompat.DEF_DISJOINT"
2105 "DEF_DIFF" > "HOLLightCompat.DEF_DIFF"
2106 "DEF_DELETE" > "HOLLightCompat.DEF_DELETE"
2107 "DEF_DECIMAL" > "HOLLight.hollight.DEF_DECIMAL"
2108 "DEF_CURRY" > "Product_Type.curry_conv"
2109 "DEF_CROSS" > "HOLLight.hollight.DEF_CROSS"
2110 "DEF_COUNTABLE" > "HOLLight.hollight.DEF_COUNTABLE"
2111 "DEF_CONSTR" > "HOLLight.hollight.DEF_CONSTR"
2112 "DEF_COND" > "HOLLightCompat.COND_DEF"
2113 "DEF_CHOICE" > "HOLLightCompat.DEF_CHOICE"
2114 "DEF_CASEWISE" > "HOLLight.hollight.DEF_CASEWISE"
2115 "DEF_CARD" > "HOLLight.hollight.DEF_CARD"
2116 "DEF_BUTLAST" > "HOLLightList.DEF_BUTLAST"
2117 "DEF_BOTTOM" > "HOLLight.hollight.DEF_BOTTOM"
2118 "DEF_BIT1" > "HOLLightCompat.BIT1_DEF"
2119 "DEF_BIT0" > "HOLLightCompat.BIT0_DEF"
2120 "DEF_BIJ" > "HOLLight.hollight.DEF_BIJ"
2121 "DEF_ASCII" > "HOLLight.hollight.DEF_ASCII"
2122 "DEF_APPEND" > "HOLLightList.DEF_APPEND"
2123 "DEF_ALL2" > "HOLLightList.DEF_ALL2"
2124 "DEF_ALL" > "HOLLightList.DEF_ALL"
2125 "DEF_-" > "HOLLightCompat.DEF_MINUS"
2126 "DEF_+" > "HOLLightCompat.DEF_PLUS"
2127 "DEF_$" > "HOLLight.hollight.DEF_$"
2128 "DECOMPOSITION" > "HOLLight.hollight.DECOMPOSITION"
2129 "DECIMAL_def" > "HOLLight.hollight.DECIMAL_def"
2130 "CROSS_def" > "HOLLight.hollight.CROSS_def"
2131 "CROSS_EQ_EMPTY" > "HOLLight.hollight.CROSS_EQ_EMPTY"
2132 "COUNTABLE_def" > "HOLLight.hollight.COUNTABLE_def"
2133 "CONS_HD_TL" > "List.hd_Cons_tl"
2134 "CONS_11" > "List.list.inject"
2135 "CONSTR_def" > "HOLLight.hollight.CONSTR_def"
2136 "CONSTR_REC" > "HOLLight.hollight.CONSTR_REC"
2137 "CONSTR_INJ" > "HOLLight.hollight.CONSTR_INJ"
2138 "CONSTR_IND" > "HOLLight.hollight.CONSTR_IND"
2139 "CONSTR_BOT" > "HOLLight.hollight.CONSTR_BOT"
2140 "CONJ_SYM" > "Groebner_Basis.dnf_3"
2141 "CONJ_ASSOC" > "HOL.conj_ac_3"
2142 "CONJ_ACI" > "HOLLight.hollight.CONJ_ACI"
2143 "COND_RATOR" > "HOLLight.hollight.COND_RATOR"
2144 "COND_RAND" > "HOL.if_distrib"
2145 "COND_ID" > "HOL.if_cancel"
2146 "COND_EXPAND" > "HOLLight.hollight.COND_EXPAND"
2147 "COND_EQ_CLAUSE" > "HOLLight.hollight.COND_EQ_CLAUSE"
2148 "COND_ELIM_THM" > "HOL.if_splits_1"
2149 "COND_CLAUSES" > "HOLLight.hollight.COND_CLAUSES"
2150 "COND_ABS" > "HOLLight.hollight.COND_ABS"
2151 "COMPONENT" > "Set.insertI1"
2152 "CHOOSE_SUBSET_STRONG" > "HOLLight.hollight.CHOOSE_SUBSET_STRONG"
2153 "CHOOSE_SUBSET" > "HOLLight.hollight.CHOOSE_SUBSET"
2154 "CHOICE_DEF" > "HOLLight.hollight.CHOICE_DEF"
2155 "CASEWISE_def" > "HOLLight.hollight.CASEWISE_def"
2156 "CART_EQ_FULL" > "HOLLight.hollight.CART_EQ_FULL"
2157 "CART_EQ" > "HOLLight.hollight.CART_EQ"
2158 "CARD_def" > "HOLLight.hollight.CARD_def"
2159 "CARD_UNION_OVERLAP_EQ" > "HOLLight.hollight.CARD_UNION_OVERLAP_EQ"
2160 "CARD_UNION_OVERLAP" > "HOLLight.hollight.CARD_UNION_OVERLAP"
2161 "CARD_UNION_LE" > "HOLLight.hollight.CARD_UNION_LE"
2162 "CARD_UNION_GEN" > "HOLLight.hollight.CARD_UNION_GEN"
2163 "CARD_UNION_EQ" > "HOLLight.hollight.CARD_UNION_EQ"
2164 "CARD_UNIONS_LE" > "HOLLight.hollight.CARD_UNIONS_LE"
2165 "CARD_UNIONS" > "HOLLight.hollight.CARD_UNIONS"
2166 "CARD_UNION" > "HOLLight.hollight.CARD_UNION"
2167 "CARD_SUBSET_LE" > "HOLLight.hollight.CARD_SUBSET_LE"
2168 "CARD_SUBSET_IMAGE" > "HOLLight.hollight.CARD_SUBSET_IMAGE"
2169 "CARD_SUBSET_EQ" > "HOLLight.hollight.CARD_SUBSET_EQ"
2170 "CARD_SUBSET" > "HOLLight.hollight.CARD_SUBSET"
2171 "CARD_PSUBSET" > "HOLLight.hollight.CARD_PSUBSET"
2172 "CARD_PRODUCT" > "HOLLight.hollight.CARD_PRODUCT"
2173 "CARD_POWERSET" > "HOLLight.hollight.CARD_POWERSET"
2174 "CARD_NUMSEG_LT" > "HOLLight.hollight.CARD_NUMSEG_LT"
2175 "CARD_NUMSEG_LEMMA" > "HOLLight.hollight.CARD_NUMSEG_LEMMA"
2176 "CARD_NUMSEG_LE" > "HOLLight.hollight.CARD_NUMSEG_LE"
2177 "CARD_NUMSEG_1" > "HOLLight.hollight.CARD_NUMSEG_1"
2178 "CARD_NUMSEG" > "HOLLight.hollight.CARD_NUMSEG"
2179 "CARD_LE_INJ" > "HOLLight.hollight.CARD_LE_INJ"
2180 "CARD_IMAGE_LE" > "HOLLight.hollight.CARD_IMAGE_LE"
2181 "CARD_IMAGE_INJ_EQ" > "HOLLight.hollight.CARD_IMAGE_INJ_EQ"
2182 "CARD_IMAGE_INJ" > "HOLLight.hollight.CARD_IMAGE_INJ"
2183 "CARD_FUNSPACE" > "HOLLight.hollight.CARD_FUNSPACE"
2184 "CARD_FINITE_IMAGE" > "HOLLight.hollight.CARD_FINITE_IMAGE"
2185 "CARD_EQ_SUM" > "HOLLight.hollight.CARD_EQ_SUM"
2186 "CARD_EQ_NSUM" > "HOLLight.hollight.CARD_EQ_NSUM"
2187 "CARD_EQ_BIJECTIONS" > "HOLLight.hollight.CARD_EQ_BIJECTIONS"
2188 "CARD_EQ_BIJECTION" > "HOLLight.hollight.CARD_EQ_BIJECTION"
2189 "CARD_EQ_0" > "HOLLight.hollight.CARD_EQ_0"
2190 "CARD_DIFF" > "HOLLight.hollight.CARD_DIFF"
2191 "CARD_DELETE" > "HOLLight.hollight.CARD_DELETE"
2192 "CARD_CROSS" > "HOLLight.hollight.CARD_CROSS"
2193 "CARD_CLAUSES" > "HOLLight.hollight.CARD_CLAUSES"
2194 "BOUNDS_NOTZERO" > "HOLLight.hollight.BOUNDS_NOTZERO"
2195 "BOUNDS_LINEAR_0" > "HOLLight.hollight.BOUNDS_LINEAR_0"
2196 "BOUNDS_LINEAR" > "HOLLight.hollight.BOUNDS_LINEAR"
2197 "BOUNDS_IGNORE" > "HOLLight.hollight.BOUNDS_IGNORE"
2198 "BOUNDS_DIVIDED" > "HOLLight.hollight.BOUNDS_DIVIDED"
2199 "BOTTOM_def" > "HOLLight.hollight.BOTTOM_def"
2200 "BOOL_CASES_AX" > "HOL.True_or_False"
2201 "BIT1_THM" > "HOLLight.hollight.BIT1_THM"
2202 "BIT1" > "HOLLight.hollight.BIT1"
2203 "BIT0_THM" > "Int.semiring_mult_2"
2204 "BIT0" > "Int.semiring_mult_2"
2205 "BIJ_def" > "HOLLight.hollight.BIJ_def"
2206 "BIJECTIVE_ON_LEFT_RIGHT_INVERSE" > "HOLLight.hollight.BIJECTIVE_ON_LEFT_RIGHT_INVERSE"
2207 "BIJECTIVE_LEFT_RIGHT_INVERSE" > "HOLLight.hollight.BIJECTIVE_LEFT_RIGHT_INVERSE"
2208 "BIJECTIONS_HAS_SIZE_EQ" > "HOLLight.hollight.BIJECTIONS_HAS_SIZE_EQ"
2209 "BIJECTIONS_HAS_SIZE" > "HOLLight.hollight.BIJECTIONS_HAS_SIZE"
2210 "BIJECTIONS_CARD_EQ" > "HOLLight.hollight.BIJECTIONS_CARD_EQ"
2211 "BETA_THM" > "HOL.eta_contract_eq"
2212 "ASCII_def" > "HOLLight.hollight.ASCII_def"
2213 "ARITH_ZERO" > "HOLLight.hollight.ARITH_ZERO"
2214 "ARITH_SUC" > "HOLLight.hollight.ARITH_SUC"
2215 "ARITH_SUB" > "HOLLight.hollight.ARITH_SUB"
2216 "ARITH_PRE" > "HOLLight.hollight.ARITH_PRE"
2217 "ARITH_ODD" > "HOLLight.hollight.ARITH_ODD"
2218 "ARITH_MULT" > "HOLLight.hollight.ARITH_MULT"
2219 "ARITH_LT" > "HOLLight.hollight.ARITH_LT"
2220 "ARITH_LE" > "HOLLight.hollight.ARITH_LE"
2221 "ARITH_EXP" > "HOLLight.hollight.ARITH_EXP"
2222 "ARITH_EVEN" > "HOLLight.hollight.ARITH_EVEN"
2223 "ARITH_EQ" > "HOLLight.hollight.ARITH_EQ"
2224 "ARITH_ADD" > "HOLLight.hollight.ARITH_ADD"
2225 "APPEND_NIL" > "List.append_Nil2"
2226 "APPEND_EQ_NIL" > "List.append_is_Nil_conv"
2227 "APPEND_BUTLAST_LAST" > "List.append_butlast_last_id"
2228 "APPEND_ASSOC" > "List.append_assoc"
2229 "AND_FORALL_THM" > "HOL.all_conj_distrib"
2230 "AND_CLAUSES" > "HOLLight.hollight.AND_CLAUSES"
2231 "AND_ALL2" > "HOLLightList.AND_ALL2"
2232 "AND_ALL" > "HOLLightList.AND_ALL"
2233 "ALL_T" > "HOLLightList.ALL_T"
2234 "ALL_MP" > "HOLLightList.ALL_MP"
2235 "ALL_MEM" > "HOLLightList.ALL_MEM"
2236 "ALL_IMP" > "HOLLightList.ALL_IMP"
2237 "ALL_EL" > "List.list_all_length"
2238 "ALL_APPEND" > "List.list_all_append"
2239 "ALL2_MAP2" > "HOLLightList.ALL2_MAP2"
2240 "ALL2_MAP" > "HOLLightList.ALL2_MAP"
2241 "ALL2_AND_RIGHT" > "HOLLightList.ALL2_AND_RIGHT"
2242 "ALL2_ALL" > "HOLLightList.ALL2_ALL"
2243 "ALL2" > "HOLLightList.ALL2"
2244 "ADMISSIBLE_UNGUARDED_PATTERN" > "HOLLight.hollight.ADMISSIBLE_UNGUARDED_PATTERN"
2245 "ADMISSIBLE_SUM" > "HOLLight.hollight.ADMISSIBLE_SUM"
2246 "ADMISSIBLE_SEQPATTERN" > "HOLLight.hollight.ADMISSIBLE_SEQPATTERN"
2247 "ADMISSIBLE_RAND" > "HOLLight.hollight.ADMISSIBLE_RAND"
2248 "ADMISSIBLE_NSUM" > "HOLLight.hollight.ADMISSIBLE_NSUM"
2249 "ADMISSIBLE_NEST" > "HOLLight.hollight.ADMISSIBLE_NEST"
2250 "ADMISSIBLE_MATCH_SEQPATTERN" > "HOLLight.hollight.ADMISSIBLE_MATCH_SEQPATTERN"
2251 "ADMISSIBLE_MATCH" > "HOLLight.hollight.ADMISSIBLE_MATCH"
2252 "ADMISSIBLE_MAP" > "HOLLight.hollight.ADMISSIBLE_MAP"
2253 "ADMISSIBLE_LAMBDA" > "HOLLight.hollight.ADMISSIBLE_LAMBDA"
2254 "ADMISSIBLE_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.ADMISSIBLE_IMP_SUPERADMISSIBLE"
2255 "ADMISSIBLE_GUARDED_PATTERN" > "HOLLight.hollight.ADMISSIBLE_GUARDED_PATTERN"
2256 "ADMISSIBLE_CONST" > "HOLLight.hollight.ADMISSIBLE_CONST"
2257 "ADMISSIBLE_COND" > "HOLLight.hollight.ADMISSIBLE_COND"
2258 "ADMISSIBLE_COMB" > "HOLLight.hollight.ADMISSIBLE_COMB"
2259 "ADMISSIBLE_BASE" > "HOLLight.hollight.ADMISSIBLE_BASE"
2260 "ADD_SYM" > "Fields.linordered_field_class.sign_simps_43"
2261 "ADD_SUC" > "Nat.add_Suc_right"
2262 "ADD_SUBR2" > "Nat.diff_add_0"
2263 "ADD_SUBR" > "HOLLight.hollight.ADD_SUBR"
2264 "ADD_SUB2" > "Nat.diff_add_inverse"
2265 "ADD_SUB" > "Nat.diff_add_inverse2"
2266 "ADD_EQ_0" > "Nat.add_is_0"
2267 "ADD_CLAUSES" > "HOLLight.hollight.ADD_CLAUSES"
2268 "ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_44"
2269 "ADD_AC" > "HOLLight.hollight.ADD_AC"
2270 "ADD_0" > "Divides.arithmetic_simps_39"
2271 "ADD1" > "Nat_Numeral.Suc_eq_plus1"
2272 "ABS_SIMP" > "HOL.refl"
2273 "ABSORPTION" > "HOLLight.hollight.ABSORPTION"
2274 ">_c_def" > "HOLLight.hollight.>_c_def"
2275 ">=_c_def" > "HOLLight.hollight.>=_c_def"
2276 "=_c_def" > "HOLLight.hollight.=_c_def"
2277 "<_c_def" > "HOLLight.hollight.<_c_def"
2278 "<=_c_def" > "HOLLight.hollight.<=_c_def"
2279 "$_def" > "HOLLight.hollight.$_def"
2290 "SET_OF_LIST_OF_SET"
2292 "RECURSION_CASEWISE_PAIRWISE"
2293 "RECURSION_CASEWISE"
2298 "LIST_OF_SET_PROPERTIES"
2299 "LENGTH_LIST_OF_SET"
2300 "HAS_SIZE_SET_OF_LIST"
2303 "FINITE_SET_OF_LIST"
2307 "DIMINDEX_HAS_SIZE_FINITE_SUM"
2308 "DIMINDEX_FINITE_SUM"
2332 "CARD_SET_OF_LIST_LE"