--- a/NEWS Sun Jul 10 21:39:03 2011 +0200
+++ b/NEWS Sun Jul 10 21:46:41 2011 +0200
@@ -149,6 +149,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.