equal
deleted
inserted
replaced
415 Riemann mapping theorem, the Vitali covering theorem, |
415 Riemann mapping theorem, the Vitali covering theorem, |
416 change-of-variables results for integration and measures. |
416 change-of-variables results for integration and measures. |
417 |
417 |
418 * Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics |
418 * Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics |
419 or real-valued functions (limits, "Big-O", etc.) automatically. |
419 or real-valued functions (limits, "Big-O", etc.) automatically. |
|
420 See also ~~/src/HOL/Real_Asymp/Manual for some documentation. |
420 |
421 |
421 * Session HOL-Types_To_Sets: more tool support (unoverload_type combines |
422 * Session HOL-Types_To_Sets: more tool support (unoverload_type combines |
422 internalize_sorts and unoverload) and larger experimental application |
423 internalize_sorts and unoverload) and larger experimental application |
423 (type based linear algebra transferred to linear algebra on subspaces). |
424 (type based linear algebra transferred to linear algebra on subspaces). |
424 |
425 |