equal
deleted
inserted
replaced
146 |
146 |
147 * Map: `empty' is no longer a constant but a syntactic abbreviation for |
147 * Map: `empty' is no longer a constant but a syntactic abbreviation for |
148 %x. None. Warning: empty_def now refers to the previously hidden definition |
148 %x. None. Warning: empty_def now refers to the previously hidden definition |
149 of the empty set. |
149 of the empty set. |
150 |
150 |
151 * Algebra: contains a new formalization of group theory, using locales with |
151 * Algebra: contains a new formalization of group theory, using locales |
152 implicit structures. Also a new, experimental summation operator for |
152 with implicit structures. Also a new formalization of ring theory and |
153 abelian groups; |
153 and univariate polynomials; |
154 |
154 |
155 * GroupTheory: deleted, since its material has been moved to Algebra; |
155 * GroupTheory: deleted, since its material has been moved to Algebra; |
156 |
156 |
157 * Complex: new directory of the complex numbers with numeric constants, |
157 * Complex: new directory of the complex numbers with numeric constants, |
158 nonstandard complex numbers, and some complex analysis, standard and |
158 nonstandard complex numbers, and some complex analysis, standard and |
163 * Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques |
163 * Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques |
164 Fleuriot); |
164 Fleuriot); |
165 |
165 |
166 * Real/HahnBanach: updated and adapted to locales; |
166 * Real/HahnBanach: updated and adapted to locales; |
167 |
167 |
168 * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and |
168 * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, |
169 Kramer); |
169 Gray and Kramer); |
170 |
170 |
171 * UNITY: added the Meier-Sanders theory of progress sets; |
171 * UNITY: added the Meier-Sanders theory of progress sets; |
172 |
172 |
173 |
173 |
174 *** ZF *** |
174 *** ZF *** |