1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
Version 3.4.4
-------------
* fixed detection of MathComp 2.5
Version 3.4.3
-------------
* ensured compatibility from Coq 8.12 to 9.0
Version 3.4.2
-------------
* ensured compatibility from Coq 8.12 to 8.20
Version 3.4.1
-------------
* ensured compatibility from Coq 8.12 to 8.19
Version 3.4.0
-------------
* added an `AbelianMonoid` structure at the bottom of the hierarchy
Version 3.3.1
-------------
* fixed compilation with ssreflect 1.17 and 2.0
Version 3.3.0
-------------
* improved support for complex arithmetic
* minimal version of Coq is now 8.12
Version 3.2.0
-------------
* added `closely` to filter over pairs of close values in place of `cauchy`
Version 3.1.0
-------------
* ensured compatibility from Coq 8.8 to Coq 8.13
* added some theorems about continuity and differentiability of elementary functions
Version 3.0.3
-------------
* ensured compatibility from Coq 8.8 to Coq 8.10
Version 3.0.2
-------------
* ensured compatibility from Coq 8.5 to Coq 8.9
Version 3.0.1
-------------
* ensured compatibility from Coq 8.5 to Coq 8.7
Version 3.0.0
-------------
* generalized `RInt` to `CompleteNormedModule`
* added `filterlimi` to express limits of implicitly-defined functions
* made `is_RInt_gen` similar to other limits and defined `RInt_gen`
Version 2.1.2
-------------
* fixed compilation with Coq 8.6; minimal version is now 8.5
Version 2.1.1
-------------
* fixed compilation with ssreflect 1.6
Version 2.1.0
-------------
* added `continuous` for expressing continuity
* modified definitions for `sum_n` and `sum_n_m`
* strengthened axioms for `AbsRing` and `NormedModule`
* added `closed` for characterizing closed sets
* added `iota` for Hilbert's operator on `CompleteSpace`
* added notation `[ _ , _ , ...]` for vectors of type `Tn`
* renamed `Markov*` lemmas to `LPO*`
* proved Abel's theorem on power series
* generalized continuity and differentiability of `RInt` in `RInt_analysis`
* added support for improper integrals in `RInt_gen`
* renamed `Limit` into `Lim_seq`
* added example `BacS2013_bonus` about matrices
Version 2.0.1
-------------
* fixed compilation with ssreflect 1.5
Version 2.0.0
-------------
* removed `is_derive` as a notation for `derivable_pt_lim`
* renamed some compatibility theorems from `_equiv` to `_Reals`
* introduced a hierarchy of number structures and topological spaces
* added complex numbers
* generalized `is_RInt`, `is_derive`, `is_domin`, etc, from reals to
arbitrary left-modules
Version 1.1.0
-------------
* expressed `locally`, `Rbar_locally`, etc, as filters
* defined limits using `filterlim` and modified predicates such as `is_lim`
accordingly
* simplified definitions of `Rbar` operators
Version 1.0.0
-------------
* initial release
|
