| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 07 Sep 2011 07:59:45 +0900 | |
| changeset 44763 | b50d5d694838 |
| parent 14516 | a183dec876ab |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"tends_real_real" > "tends_real_real_def" |
|
7 |
"diffl" > "diffl_def" |
|
8 |
"differentiable" > "differentiable_def" |
|
9 |
"contl" > "contl_def" |
|
10 |
||
11 |
const_maps |
|
12 |
"tends_real_real" > "HOL4Real.lim.tends_real_real" |
|
13 |
"diffl" > "HOL4Real.lim.diffl" |
|
14 |
"differentiable" > "HOL4Real.lim.differentiable" |
|
15 |
"contl" > "HOL4Real.lim.contl" |
|
16 |
||
17 |
thm_maps |
|
18 |
"tends_real_real_def" > "HOL4Real.lim.tends_real_real_def" |
|
19 |
"tends_real_real" > "HOL4Real.lim.tends_real_real" |
|
20 |
"diffl_def" > "HOL4Real.lim.diffl_def" |
|
21 |
"diffl" > "HOL4Real.lim.diffl" |
|
22 |
"differentiable_def" > "HOL4Real.lim.differentiable_def" |
|
23 |
"differentiable" > "HOL4Real.lim.differentiable" |
|
24 |
"contl_def" > "HOL4Real.lim.contl_def" |
|
25 |
"contl" > "HOL4Real.lim.contl" |
|
26 |
"ROLLE" > "HOL4Real.lim.ROLLE" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
14516
diff
changeset
|
27 |
"MVT_LEMMA" > "Deriv.lemma_MVT" |
| 14516 | 28 |
"MVT" > "HOL4Real.lim.MVT" |
29 |
"LIM_X" > "HOL4Real.lim.LIM_X" |
|
30 |
"LIM_UNIQ" > "HOL4Real.lim.LIM_UNIQ" |
|
31 |
"LIM_TRANSFORM" > "HOL4Real.lim.LIM_TRANSFORM" |
|
32 |
"LIM_SUB" > "HOL4Real.lim.LIM_SUB" |
|
33 |
"LIM_NULL" > "HOL4Real.lim.LIM_NULL" |
|
34 |
"LIM_NEG" > "HOL4Real.lim.LIM_NEG" |
|
35 |
"LIM_MUL" > "HOL4Real.lim.LIM_MUL" |
|
36 |
"LIM_INV" > "HOL4Real.lim.LIM_INV" |
|
37 |
"LIM_EQUAL" > "HOL4Real.lim.LIM_EQUAL" |
|
38 |
"LIM_DIV" > "HOL4Real.lim.LIM_DIV" |
|
39 |
"LIM_CONST" > "HOL4Real.lim.LIM_CONST" |
|
40 |
"LIM_ADD" > "HOL4Real.lim.LIM_ADD" |
|
41 |
"LIM" > "HOL4Real.lim.LIM" |
|
42 |
"IVT2" > "HOL4Real.lim.IVT2" |
|
43 |
"IVT" > "HOL4Real.lim.IVT" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
14516
diff
changeset
|
44 |
"INTERVAL_LEMMA" > "Deriv.lemma_interval" |
| 14516 | 45 |
"INTERVAL_CLEMMA" > "HOL4Real.lim.INTERVAL_CLEMMA" |
46 |
"INTERVAL_ABS" > "HOL4Real.lim.INTERVAL_ABS" |
|
47 |
"DIFF_XM1" > "HOL4Real.lim.DIFF_XM1" |
|
48 |
"DIFF_X" > "HOL4Real.lim.DIFF_X" |
|
49 |
"DIFF_UNIQ" > "HOL4Real.lim.DIFF_UNIQ" |
|
50 |
"DIFF_SUM" > "HOL4Real.lim.DIFF_SUM" |
|
51 |
"DIFF_SUB" > "HOL4Real.lim.DIFF_SUB" |
|
52 |
"DIFF_POW" > "HOL4Real.lim.DIFF_POW" |
|
53 |
"DIFF_NEG" > "HOL4Real.lim.DIFF_NEG" |
|
54 |
"DIFF_MUL" > "HOL4Real.lim.DIFF_MUL" |
|
55 |
"DIFF_LMIN" > "HOL4Real.lim.DIFF_LMIN" |
|
56 |
"DIFF_LMAX" > "HOL4Real.lim.DIFF_LMAX" |
|
57 |
"DIFF_LINC" > "HOL4Real.lim.DIFF_LINC" |
|
58 |
"DIFF_LDEC" > "HOL4Real.lim.DIFF_LDEC" |
|
59 |
"DIFF_LCONST" > "HOL4Real.lim.DIFF_LCONST" |
|
60 |
"DIFF_ISCONST_END" > "HOL4Real.lim.DIFF_ISCONST_END" |
|
61 |
"DIFF_ISCONST_ALL" > "HOL4Real.lim.DIFF_ISCONST_ALL" |
|
62 |
"DIFF_ISCONST" > "HOL4Real.lim.DIFF_ISCONST" |
|
63 |
"DIFF_INVERSE_OPEN" > "HOL4Real.lim.DIFF_INVERSE_OPEN" |
|
64 |
"DIFF_INVERSE_LT" > "HOL4Real.lim.DIFF_INVERSE_LT" |
|
65 |
"DIFF_INVERSE" > "HOL4Real.lim.DIFF_INVERSE" |
|
66 |
"DIFF_INV" > "HOL4Real.lim.DIFF_INV" |
|
67 |
"DIFF_DIV" > "HOL4Real.lim.DIFF_DIV" |
|
68 |
"DIFF_CONT" > "HOL4Real.lim.DIFF_CONT" |
|
69 |
"DIFF_CONST" > "HOL4Real.lim.DIFF_CONST" |
|
70 |
"DIFF_CMUL" > "HOL4Real.lim.DIFF_CMUL" |
|
71 |
"DIFF_CHAIN" > "HOL4Real.lim.DIFF_CHAIN" |
|
72 |
"DIFF_CARAT" > "HOL4Real.lim.DIFF_CARAT" |
|
73 |
"DIFF_ADD" > "HOL4Real.lim.DIFF_ADD" |
|
74 |
"CONT_SUB" > "HOL4Real.lim.CONT_SUB" |
|
75 |
"CONT_NEG" > "HOL4Real.lim.CONT_NEG" |
|
76 |
"CONT_MUL" > "HOL4Real.lim.CONT_MUL" |
|
77 |
"CONT_INVERSE" > "HOL4Real.lim.CONT_INVERSE" |
|
78 |
"CONT_INV" > "HOL4Real.lim.CONT_INV" |
|
79 |
"CONT_INJ_RANGE" > "HOL4Real.lim.CONT_INJ_RANGE" |
|
80 |
"CONT_INJ_LEMMA2" > "HOL4Real.lim.CONT_INJ_LEMMA2" |
|
81 |
"CONT_INJ_LEMMA" > "HOL4Real.lim.CONT_INJ_LEMMA" |
|
82 |
"CONT_HASSUP" > "HOL4Real.lim.CONT_HASSUP" |
|
83 |
"CONT_DIV" > "HOL4Real.lim.CONT_DIV" |
|
84 |
"CONT_CONST" > "HOL4Real.lim.CONT_CONST" |
|
85 |
"CONT_COMPOSE" > "HOL4Real.lim.CONT_COMPOSE" |
|
86 |
"CONT_BOUNDED" > "HOL4Real.lim.CONT_BOUNDED" |
|
87 |
"CONT_ATTAINS_ALL" > "HOL4Real.lim.CONT_ATTAINS_ALL" |
|
88 |
"CONT_ATTAINS2" > "HOL4Real.lim.CONT_ATTAINS2" |
|
89 |
"CONT_ATTAINS" > "HOL4Real.lim.CONT_ATTAINS" |
|
90 |
"CONT_ADD" > "HOL4Real.lim.CONT_ADD" |
|
91 |
"CONTL_LIM" > "HOL4Real.lim.CONTL_LIM" |
|
92 |
||
93 |
end |