| author | wenzelm |
| Sat, 03 Mar 2012 22:53:24 +0100 | |
| changeset 46793 | 3bbc156823dd |
| parent 46787 | 3d3d8f8929a7 |
| permissions | -rw-r--r-- |
| 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" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
17694
diff
changeset
|
109 |
"BOLZANO_LEMMA" > "Deriv.lemma_BOLZANO" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
17694
diff
changeset
|
110 |
"ABS_NEG_LEMMA" > "Series.rabs_ratiotest_lemma" |
| 14516 | 111 |
|
112 |
end |