|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"sums" > "sums_def"
|
|
|
7 |
"summable" > "summable_def"
|
|
|
8 |
"suminf" > "suminf_def"
|
|
|
9 |
"subseq" > "subseq_def"
|
|
|
10 |
"mono" > "mono_def"
|
|
|
11 |
"lim" > "lim_def"
|
|
17694
|
12 |
"hol4-->" > "hol4-->_def"
|
|
14516
|
13 |
"convergent" > "convergent_def"
|
|
|
14 |
"cauchy" > "cauchy_def"
|
|
|
15 |
|
|
|
16 |
const_maps
|
|
|
17 |
"sums" > "HOL4Real.seq.sums"
|
|
|
18 |
"summable" > "HOL4Real.seq.summable"
|
|
|
19 |
"suminf" > "HOL4Real.seq.suminf"
|
|
|
20 |
"subseq" > "HOL4Real.seq.subseq"
|
|
|
21 |
"mono" > "HOL4Real.seq.mono"
|
|
|
22 |
"lim" > "HOL4Real.seq.lim"
|
|
17694
|
23 |
"hol4-->" > "HOL4Real.seq.hol4-->"
|
|
14516
|
24 |
"convergent" > "HOL4Real.seq.convergent"
|
|
|
25 |
"cauchy" > "HOL4Real.seq.cauchy"
|
|
17694
|
26 |
|
|
|
27 |
const_renames
|
|
|
28 |
"-->" > "hol4-->"
|
|
14516
|
29 |
|
|
|
30 |
thm_maps
|
|
|
31 |
"tends_num_real" > "HOL4Real.seq.tends_num_real"
|
|
|
32 |
"sums_def" > "HOL4Real.seq.sums_def"
|
|
|
33 |
"sums" > "HOL4Real.seq.sums"
|
|
|
34 |
"summable_def" > "HOL4Real.seq.summable_def"
|
|
|
35 |
"summable" > "HOL4Real.seq.summable"
|
|
|
36 |
"suminf_def" > "HOL4Real.seq.suminf_def"
|
|
|
37 |
"suminf" > "HOL4Real.seq.suminf"
|
|
|
38 |
"subseq_def" > "HOL4Real.seq.subseq_def"
|
|
|
39 |
"subseq" > "HOL4Real.seq.subseq"
|
|
|
40 |
"mono_def" > "HOL4Real.seq.mono_def"
|
|
|
41 |
"mono" > "HOL4Real.seq.mono"
|
|
|
42 |
"lim_def" > "HOL4Real.seq.lim_def"
|
|
|
43 |
"lim" > "HOL4Real.seq.lim"
|
|
17694
|
44 |
"hol4-->_def" > "HOL4Real.seq.hol4-->_def"
|
|
14516
|
45 |
"convergent_def" > "HOL4Real.seq.convergent_def"
|
|
|
46 |
"convergent" > "HOL4Real.seq.convergent"
|
|
|
47 |
"cauchy_def" > "HOL4Real.seq.cauchy_def"
|
|
|
48 |
"cauchy" > "HOL4Real.seq.cauchy"
|
|
|
49 |
"SUM_UNIQ" > "HOL4Real.seq.SUM_UNIQ"
|
|
|
50 |
"SUM_SUMMABLE" > "HOL4Real.seq.SUM_SUMMABLE"
|
|
|
51 |
"SUMMABLE_SUM" > "HOL4Real.seq.SUMMABLE_SUM"
|
|
|
52 |
"SUBSEQ_SUC" > "HOL4Real.seq.SUBSEQ_SUC"
|
|
|
53 |
"SER_ZERO" > "HOL4Real.seq.SER_ZERO"
|
|
|
54 |
"SER_SUB" > "HOL4Real.seq.SER_SUB"
|
|
|
55 |
"SER_RATIO" > "HOL4Real.seq.SER_RATIO"
|
|
|
56 |
"SER_POS_LT_PAIR" > "HOL4Real.seq.SER_POS_LT_PAIR"
|
|
|
57 |
"SER_POS_LT" > "HOL4Real.seq.SER_POS_LT"
|
|
|
58 |
"SER_POS_LE" > "HOL4Real.seq.SER_POS_LE"
|
|
|
59 |
"SER_PAIR" > "HOL4Real.seq.SER_PAIR"
|
|
|
60 |
"SER_OFFSET" > "HOL4Real.seq.SER_OFFSET"
|
|
|
61 |
"SER_NEG" > "HOL4Real.seq.SER_NEG"
|
|
|
62 |
"SER_LE2" > "HOL4Real.seq.SER_LE2"
|
|
|
63 |
"SER_LE" > "HOL4Real.seq.SER_LE"
|
|
|
64 |
"SER_GROUP" > "HOL4Real.seq.SER_GROUP"
|
|
|
65 |
"SER_COMPARA" > "HOL4Real.seq.SER_COMPARA"
|
|
|
66 |
"SER_COMPAR" > "HOL4Real.seq.SER_COMPAR"
|
|
|
67 |
"SER_CMUL" > "HOL4Real.seq.SER_CMUL"
|
|
|
68 |
"SER_CDIV" > "HOL4Real.seq.SER_CDIV"
|
|
|
69 |
"SER_CAUCHY" > "HOL4Real.seq.SER_CAUCHY"
|
|
|
70 |
"SER_ADD" > "HOL4Real.seq.SER_ADD"
|
|
|
71 |
"SER_ACONV" > "HOL4Real.seq.SER_ACONV"
|
|
|
72 |
"SER_ABS" > "HOL4Real.seq.SER_ABS"
|
|
|
73 |
"SER_0" > "HOL4Real.seq.SER_0"
|
|
|
74 |
"SEQ_UNIQ" > "HOL4Real.seq.SEQ_UNIQ"
|
|
|
75 |
"SEQ_SUC" > "HOL4Real.seq.SEQ_SUC"
|
|
|
76 |
"SEQ_SUBLE" > "HOL4Real.seq.SEQ_SUBLE"
|
|
|
77 |
"SEQ_SUB" > "HOL4Real.seq.SEQ_SUB"
|
|
|
78 |
"SEQ_SBOUNDED" > "HOL4Real.seq.SEQ_SBOUNDED"
|
|
|
79 |
"SEQ_POWER_ABS" > "HOL4Real.seq.SEQ_POWER_ABS"
|
|
|
80 |
"SEQ_POWER" > "HOL4Real.seq.SEQ_POWER"
|
|
|
81 |
"SEQ_NEG_CONV" > "HOL4Real.seq.SEQ_NEG_CONV"
|
|
|
82 |
"SEQ_NEG_BOUNDED" > "HOL4Real.seq.SEQ_NEG_BOUNDED"
|
|
|
83 |
"SEQ_NEG" > "HOL4Real.seq.SEQ_NEG"
|
|
|
84 |
"SEQ_MUL" > "HOL4Real.seq.SEQ_MUL"
|
|
|
85 |
"SEQ_MONOSUB" > "HOL4Real.seq.SEQ_MONOSUB"
|
|
|
86 |
"SEQ_LIM" > "HOL4Real.seq.SEQ_LIM"
|
|
|
87 |
"SEQ_LE" > "HOL4Real.seq.SEQ_LE"
|
|
|
88 |
"SEQ_INV0" > "HOL4Real.seq.SEQ_INV0"
|
|
|
89 |
"SEQ_INV" > "HOL4Real.seq.SEQ_INV"
|
|
|
90 |
"SEQ_ICONV" > "HOL4Real.seq.SEQ_ICONV"
|
|
|
91 |
"SEQ_DIV" > "HOL4Real.seq.SEQ_DIV"
|
|
|
92 |
"SEQ_DIRECT" > "HOL4Real.seq.SEQ_DIRECT"
|
|
|
93 |
"SEQ_CONST" > "HOL4Real.seq.SEQ_CONST"
|
|
|
94 |
"SEQ_CBOUNDED" > "HOL4Real.seq.SEQ_CBOUNDED"
|
|
|
95 |
"SEQ_CAUCHY" > "HOL4Real.seq.SEQ_CAUCHY"
|
|
|
96 |
"SEQ_BOUNDED_2" > "HOL4Real.seq.SEQ_BOUNDED_2"
|
|
|
97 |
"SEQ_BOUNDED" > "HOL4Real.seq.SEQ_BOUNDED"
|
|
|
98 |
"SEQ_BCONV" > "HOL4Real.seq.SEQ_BCONV"
|
|
|
99 |
"SEQ_ADD" > "HOL4Real.seq.SEQ_ADD"
|
|
|
100 |
"SEQ_ABS_IMP" > "HOL4Real.seq.SEQ_ABS_IMP"
|
|
|
101 |
"SEQ_ABS" > "HOL4Real.seq.SEQ_ABS"
|
|
|
102 |
"SEQ" > "HOL4Real.seq.SEQ"
|
|
|
103 |
"NEST_LEMMA_UNIQ" > "HOL4Real.seq.NEST_LEMMA_UNIQ"
|
|
|
104 |
"NEST_LEMMA" > "HOL4Real.seq.NEST_LEMMA"
|
|
|
105 |
"MONO_SUC" > "HOL4Real.seq.MONO_SUC"
|
|
|
106 |
"MAX_LEMMA" > "HOL4Real.seq.MAX_LEMMA"
|
|
|
107 |
"GP_FINITE" > "HOL4Real.seq.GP_FINITE"
|
|
|
108 |
"GP" > "HOL4Real.seq.GP"
|
|
|
109 |
"BOLZANO_LEMMA" > "HOL4Real.seq.BOLZANO_LEMMA"
|
|
|
110 |
"ABS_NEG_LEMMA" > "HOL4Real.seq.ABS_NEG_LEMMA"
|
|
|
111 |
|
|
|
112 |
end
|