equal
deleted
inserted
replaced
391 INCOMPATIBILITY. |
391 INCOMPATIBILITY. |
392 |
392 |
393 * Session HOL-Analysis: infinite products, Moebius functions, the |
393 * Session HOL-Analysis: infinite products, Moebius functions, the |
394 Riemann mapping theorem, the Vitali covering theorem, |
394 Riemann mapping theorem, the Vitali covering theorem, |
395 change-of-variables results for integration and measures. |
395 change-of-variables results for integration and measures. |
|
396 |
|
397 * Session HOL-Types_To_Sets: more tool support |
|
398 (unoverload_type combines internalize_sorts and unoverload) and larger |
|
399 experimental application (type based linear algebra transferred to linear |
|
400 algebra on subspaces). |
396 |
401 |
397 |
402 |
398 *** ML *** |
403 *** ML *** |
399 |
404 |
400 * Operation Export.export emits theory exports (arbitrary blobs), which |
405 * Operation Export.export emits theory exports (arbitrary blobs), which |