--- a/NEWS Fri Sep 10 23:18:51 2021 +0200
+++ b/NEWS Sat Sep 11 13:04:32 2021 +0200
@@ -248,6 +248,9 @@
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
accumulation of items.
+* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
+corresponding ML values, notably as arguments for Thm.instantiate etc.
+
* The "build" combinators of various data structures help to build
content from bottom-up, by applying an "add" function the "empty" value.
For example: