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"
|
|
27 |
"MVT_LEMMA" > "HOL4Real.lim.MVT_LEMMA"
|
|
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"
|
|
44 |
"INTERVAL_LEMMA" > "HOL4Real.lim.INTERVAL_LEMMA"
|
|
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
|