--- a/NEWS Sun Jul 10 17:58:11 2011 +0200
+++ b/NEWS Sun Jul 10 20:59:04 2011 +0200
@@ -146,6 +146,12 @@
*** ML ***
+* The inner syntax of sort/type/term/prop supports inlined YXML
+representations within quoted string tokens. By encoding logical
+entities via Term_XML (in ML or Scala) concrete syntax can be
+bypassed, which is particularly useful for producing bits of text
+under external program control.
+
* Antiquotations for ML and document preparation are managed as theory
data, which requires explicit setup.