* The ML antiquotation prints type-checked ML expressions verbatim.

--- a/NEWS	Thu Aug 18 11:17:51 2005 +0200
+++ b/NEWS	Thu Aug 18 11:59:17 2005 +0200
@@ -83,12 +83,15 @@
   @{term_style style term} and @{thm_style style thm} print a term or
   theorem applying a "style" to it
 
+  @{ML text}
+
 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
 definitions, equations, inequations etc., 'concl' printing only the
 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9'
 to print the specified premise.  TermStyle.add_style provides an ML
 interface for introducing further styles.  See also the "LaTeX Sugar"
-document practical applications.
+document practical applications.  The ML antiquotation prints
+type-checked ML expressions verbatim.
 
 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
 a proof context.