equal
deleted
inserted
replaced
302 |
302 |
303 * Theory Library/Extended_Reals replaces now the positive extended |
303 * Theory Library/Extended_Reals replaces now the positive extended |
304 reals found in probability theory. This file is extended by |
304 reals found in probability theory. This file is extended by |
305 Multivariate_Analysis/Extended_Real_Limits. |
305 Multivariate_Analysis/Extended_Real_Limits. |
306 |
306 |
307 * Old 'recdef' package has been moved to theory Library/Old_Recdef, |
307 * Theory Library/Old_Recdef: old 'recdef' package has been moved here, |
308 from where it must be imported explicitly. INCOMPATIBILITY. |
308 from where it must be imported explicitly if it is really required. |
|
309 INCOMPATIBILITY. |
309 |
310 |
310 * Theory Library/Wfrec: well-founded recursion combinator "wfrec" has |
311 * Theory Library/Wfrec: well-founded recursion combinator "wfrec" has |
311 been moved here. INCOMPATIBILITY. |
312 been moved here. INCOMPATIBILITY. |
312 |
313 |
313 * Theory Library/Saturated provides type of numbers with saturated |
314 * Theory Library/Saturated provides type of numbers with saturated |