diff -r 1bad08165162 -r d9cbc1e8644d NEWS
--- 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 ***