| changeset 68522 | d9cbc1e8644d |
| parent 68515 | 0854edc4d415 |
| child 68523 | ccacc84e0251 |
--- a/NEWS Wed Jun 27 10:18:03 2018 +0200 +++ b/NEWS Wed Jun 27 11:16:43 2018 +0200 @@ -394,6 +394,11 @@ Riemann mapping theorem, the Vitali covering theorem, change-of-variables results for integration and measures. +* Session HOL-Types_To_Sets: more tool support +(unoverload_type combines internalize_sorts and unoverload) and larger +experimental application (type based linear algebra transferred to linear +algebra on subspaces). + *** ML ***